Ah... now I understand your concern; I should have written something like: where K +_t K' denotes the set of constraints from K plus those from K' that have type variables reachable from t.
instead of: where K +_t K' denotes the constraint-set obtained by adding from K' only constraints with type variables reachable from t. Cheers, Carlos On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer <lrpal...@gmail.com> wrote: > I am not totally sure if I understand your proposal correctly, but if > I do, then it has a flaw. Consider: > > class Boolable a where > boolify :: a -> Bool > > class O a where > o :: a > > main = print $ boolify o > > It seems like under your proposal this should not be a type error. > But if that is so, then what is its output? > > Luke > > On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao > <carlos.cama...@gmail.com> wrote: > > Hi. Consider for example an expression e0 like: > > > > fst (True,e) > > > > where e is any expression. > > > > e0 should have type Bool IMHO irrespectively of the type of e. In Haskell > > this is the case if e's type is monomorphic, or polymorphic, or > > constrained and there is a default in the current module that removes > > the constraints. However, e0 is not type-correct if e has a > > constrained type and the constraints are not subject to > > defaulting. For example: > > > > class O a where o::a > > main = print $ fst(True,o) > > > > generates a type error; in GHC: > > > > Ambiguous type variable `a' in the constraint: > > `O a' arising from a use of `o' at ... > > Probable fix: add a type signature that fixes these type variable(s) > > > > A solution (that avoids type signatures) can be given as follows. > > > > The type of f e, for f of type, say, K=>t'->t and e of type K'=> t' > > should be: > > > > K +_t K' => t (not K U K' => t) > > > > where K +_t K' denotes the constraint-set obtained by adding from K' > > only constraints with type variables reachable from t. > > > > (A type variable is reachable if it appears in the same constraint as > > either a type variable free in the type, or another reachable type > > variable.) > > > > Comments? Does that need and deserve a proposal? > > > > Cheers, > > > > Carlos > > > > _______________________________________________ > > Haskell-Cafe mailing list > > haskell-c...@haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > >
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
