[Haskell] Functional dependencies and type inference (2)

[kahl at cas.mcmaster.ca]

 Louis-Julien Guillemette <guillelj at 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