Simon Peyton-Jones wrote: > | > {-# OPTIONS -fglasgow-exts #-} > | > > | > class C a b c | a b -> c where > | > foo :: (a, b) -> c > | > > | > instance C a a r => C a (b, c) r where > | > foo (a, (b, c)) = foo (a, a) > > You are already on dodgy ground here, because the instance decl doesn't > guarantee that the bit before the => is smaller than the bit after the > =>. E.g. context reduction could go: > C (Int,Int) (Bool, Bool) r > --> C (Int,Int) (Int,Int) r > --> C (Int,Int) (Int,Int) r > > So [Point 1]: GHC should require -fallow-undecidable-instances if you > use repeated type variables before the =>.
Yes, I think that would be a good idea. > | Now, in GHCi (version 6.4), > | > | > *FDs> let bar x = foo ((x, x), (x, x)) > | > *FDs> :t bar > | > bar :: (C (a, a) (a, a) c) => a -> c > | > | but GHC is also happy to accept the more general type > | > | > bar :: a -> c > | > bar x = foo ((x, x), (x, x)) > > There are two separate things going on here > > [Point 2] GHC postpones context reduction until it's forced to do it > (except if a single step will eliminate the dictionary altogether). > Example: > > data T a = T a > instance Eq (T a) > bar x = [T x] == [] > > GHC will *infer* bar :: Eq [T a] => a -> Bool, but it will happily > *check* > bar :: a -> Bool > bar x = [T x] == [] > > The reason for this lazy context reduction is overlapping instances; in > principle there might be more instances for Eq [T a] at bar's call site. > > But now I look at it again, I think it would be OK to postpone context > reduction only if there actually were overlapping instances (right here > at bar's defn). That might be a good idea because it'd give less > confusing types perhaps. > > However, note that the two types are indeed equivalent -- both are more > general than the other. It's like saying (Eq Int => t) <= t, > and vice versa. Semantically, I understand that the constraint "C ((x, x), (x, x) a)" does not constrain the two type variables "x" and "a" (and hence, the two types are equivalent), but I don't see how you can derive that with the constraint entailment rules \theta \in P ------------ P ||- \theta P ||- forall a.\theta --------------------- P || [t/a]\theta P || p => \phi P ||- p ------------------------ P ||- \phi which I thought are those underlying GHC's type system. > | Again, in GHCi, > | > | > *FDs> let bar x = foo ((x::Int, x), (x, x)) > | > *FDs> :t bar > | > bar :: Int -> () > | > | (which by itself is bizarre) > > This is the first time when the functional dependency plays a role. > >From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int) > c), and the type (Int -> c). Now GHC tries to decide what to quantify > over. Shall we quantify over c? Well, no. GHC never quantifies over > type variables that are free in the environment (of course) OR are fixed > by functional dependencies from type variables free in the environment. > In this case the functional dependencies tell us that since (Int,Int) is > obviously completely fixed, then there's no point in quantifying over c. > > > So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is > satisfied via the recursive dictionary thing, leaving 'c' completely > unconstrained. So GHC chooses c to be (), because it doesn't like to > leave programs with completely free type variables. > > | but it also accepts > | > | > bar :: Int -> c > | > bar x = foo ((x::Int, x), (x, x)) > > Here you are *telling* GHC what to quantify over, so the inference of > what to quantify doesn't happen. I accept that this is the process by which GHC computes these types, but it does violate the principal types property, doesn't it? The relation Int -> () <= forall c. Int -> c does not hold. Summary ~~~~~~~ So it seems to me that * MPTCs with recursive dictionary construction seem to require a semantic model of subsumption (as the normal constraint entailment rules would lead to infinite trees). * MPTCs with recursive dictionary construction and FDs break principal types. I guess that's all ok provided GHC enforces the use of -fallow-undecidable-instances for any instances that need recursive dictionaries. Manuel _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users