Louis-Julien Guillemette <guillelj@iro.umontreal.ca> wrote:
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 ()
[...]
Couldn't match the rigid variable `cps_t' against `Bool'
[...]
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?
My way around this is to replace instance derivations by GADT elements, something like: data CpsForm :: * -> * -> * where CpsBool :: CpsForm Bool Bool cps :: CpsForm t cps_t -> Term t -> (Term cps_t -> Term ()) -> Term () YMMV! Wolfram