Say we are using a GADT to represent a simple language of boolean
constants and conditionals,
data Term a where
B :: Bool -> Term Bool
Cnd :: Term Bool -> Term t -> Term t -> Term t
and we would like to perform a type-safe CPS conversion over this language. We
encode the relationship between the types in the source language and those in
the CPS-converted language using a class and a fundep:
class CpsForm a b | a -> b
instance CpsForm Bool Bool
A natural formulation of the type of the CPS transformation would be
cps :: CpsForm t cps_t => Term t -> (Term cps_t -> Term ()) -> Term ()
cps (B b) c = c (B b) -- doesn't type-check!
cps (Cnd p q r) c = cps p (\p' -> Cnd p' (cps q c) (cps r c))
-- type-checks OK
but the first clause of the function doesn't type-check:
Couldn't match the rigid variable `cps_t' against `Bool'
`cps_t' is bound by the type signature for `cps'
Expected type: Term cps_t
Inferred type: Term Bool
In the application `B b'
In the first argument of `c', namely `(B b)'
On the contrary, if we push the (otherwise implicit) quantifier inside the
parentheses:
cps' :: Term t
-> (forall cps_t . CpsForm t cps_t => Term cps_t -> Term ())
-> Term ()
cps' (B b) c = c (B b) -- type-checks OK
cps' (Cnd p q r) c = cps' p (\p' -> Cnd p' (cps' q c) (cps' r c))
-- doesn't type-check!
then the second clause fails to type-check:
Couldn't match the rigid variable `cps_t' against `Bool'
`cps_t' is bound by the polymorphic type `forall cps_t.
(CpsForm t cps_t) =>
Term cps_t -> Term ()'
Expected type: Term Bool
Inferred type: Term cps_t
In the first argument of `Cnd', namely `p''
In a lambda abstraction: \ p' -> Cnd p' (cps' q c) (cps' r c)
This case seems to be an instance of a problem discussed earlier.
(http://www.haskell.org/pipermail/haskell-cafe/2005-August/011053.html)
Any suggestion on a way to get around this problem in current Haskell?
And, any hope to get this fixed in a future release of GHC?
Thanks
Louis-Julien
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
