Constraint error related to type family and higher-rank type

[Simon Peyton-Jones]

This is delicate.  First, make sure you read the paper "Modular type inference with local assumptions" (on my home page).

Now, typechecking v's RHS will generate this implication constraint (see the paper):

   (forall b. (C alpha b, TF b ~ Y) => C A beta, TF beta ~ Y, b~beta)

where 'alpha' is a unification variable arising from instantiating the call to 'f', and 'beta' is the unification variable arising from instantiating the call to 'u'.

We can fix beta := b, and the constrain simplifies to
   (forall b. (C alpha b, TF b ~ Y) => C A b)

Now, the functional dependency generates an additional equality constraint (alpha~A):
   (forall b. (C alpha b, TF b ~ Y) => C A b, alpha ~ A)

BUT alpha comes from "outside" the implication so it is "untouchable", in the vocabulary of the paper.   So we are stuck. 

If we don't have the constraint (TF b ~ Y), then the implication has no equality constraints, and in that situation GHC will "float" the equality (alpha ~ A) outside the implication, giving
   alpha~A, (forall b. (C alpha b, TF b ~ Y) => C A b)

Now alpha is not untouchable, so we can set alpha := A, and after that all is well.

We can't do the equality-floating thing if there are equalities in the "givens" of the implication, for reasons explained in the paper (we'd get spurious errors in the case of GADTs and the like).  In this case the (TF b ~ Y) can't really affect matters, but it's hard to be sure in general.

Simon


|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Tsuyoshi Ito
|  Sent: 03 September 2012 18:41
|  To: glasgow-haskell-users at haskell.org
|  Subject: Constraint error related to type family and higher-rank type
|  
|  Hello,
|  
|  Can anyone please explain why the following code is rejected by GHC (7.4.1)?
|  
|  The same code is also available at https://gist.github.com/3606849.
|  
|  -----
|  {-# LANGUAGE FlexibleContexts #-}
|  {-# LANGUAGE FunctionalDependencies #-}
|  {-# LANGUAGE MultiParamTypeClasses #-}
|  {-# LANGUAGE RankNTypes #-}
|  {-# LANGUAGE TypeFamilies #-}
|  
|  module Test1 where
|  
|  class C a b | b -> a
|  
|  data A = A
|  data X = X
|  data Y = Y
|  
|  type family TF b
|  
|  f :: (forall b. (C a b, TF b ~ Y) => b) -> X
|  f _ = undefined
|  
|  u :: (C A b, TF b ~ Y) => b
|  u = undefined
|  
|  v :: X
|  v = f u -- This line causes an error (see below)
|  -----
|  
|  (1) GHC rejects this code with the following error message.
|  
|  Test1.hs:24:7:
|      Could not deduce (C A b) arising from a use of `u'
|      from the context (C a_c b, TF b ~ Y)
|        bound by a type expected by the context: (C a_c b, TF b ~ Y) => b
|        at Test1.hs:24:5-7
|      Possible fix:
|        add (C A b) to the context of
|          a type expected by the context: (C a_c b, TF b ~ Y) => b
|        or add an instance declaration for (C A b)
|      In the first argument of `f', namely `u'
|      In the expression: f u
|      In an equation for `v': v = f u
|  
|  (2) If I remove "TF b ~ Y" from the type of the argument of f and the type of u,
|      then the code compiles.
|      This suggests that the error message in (1) might not be the accurate
|      description of the problem.
|  
|  (3) If I write "(f :: (forall b. (C A b, TF b ~ Y) => b) -> X)"
|  instead of just "f"
|      in the definition of v, then GHC reports a different error:
|  
|  Test1.hs:24:6:
|      Cannot deal with a type function under a forall type:
|      forall b. (C A b, TF b ~ Y) => b
|      In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X
|      In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
|      In an equation for `v':
|          v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
|  
|  Item (3) might be related to a fixed Ticket #4310:
|  http://hackage.haskell.org/trac/ghc/ticket/4310#comment:2
|  
|  Best regards,
|    Tsuyoshi
|  
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  Glasgow-haskell-users at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users