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 <[email protected]> wrote: > 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: [email protected] > [mailto:glasgow-haskell-users- > | [email protected]] On Behalf Of Tsuyoshi Ito > | Sent: 03 September 2012 18:41 > | To: [email protected] > | 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 > | [email protected] > | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
