Constraint error related to type family and higherrank type
Simon PeytonJones
simonpj at microsoft.com
Mon Sep 3 22:51:38 CEST 2012
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 equalityfloating 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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of Tsuyoshi Ito
 Sent: 03 September 2012 18:41
 To: glasgowhaskellusers at haskell.org
 Subject: Constraint error related to type family and higherrank 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:57
 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

 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list