Dear Simon,
Thank you for the detailed reply. For now, from your reply, I
understand that this issue is a result of the careful tradeoff between
completeness and decidability/efficiency of type checker, and it
cannot be easily avoided. I will read your paper “Modular type
inference with local assumptions” when I have more time. I just
glanced at the paper so far, and although I have to admit that its
length is scary, it looks at least approachable even for a non-expert
in programming languages like me.
By the way, I had a chance to test the same code with GHC 7.6.1-rc1
(7.6.0.20120810; 64-bit Windows), and noticed an error message which
looked strange to me in a variation of the code (which I described in
case (3) in the previous message). In case it might be a problem with
GHC, I reported it as http://hackage.haskell.org/trac/ghc/ticket/7220.
Best regards,
Tsuyoshi
On Mon, Sep 3, 2012 at 4:51 PM, 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@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Tsuyoshi Ito | Sent: 03 September 2012 18:41 | To: glasgow-haskell-users@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users