Haskell: Why does GHC not infer type in this typeclass with fundeps?

Question

I'm trying to use typeclasses and functional dependencies to get a type function that can transform say, Int to Cont Int in the code below, then use it in another typeclass as shown below.

{-# LANGUAGE KindSignatures, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}

newtype TestData a b = TestData b
newtype Cont a = Cont a

class TypeConv (repr :: * -> *) a b | repr a -> b where
class Lift repr a where
    liftOp :: (TypeConv repr a a') => a -> repr a'

instance TypeConv (TestData a) Int (Cont Int) where

instance Lift (TestData a) Int where
    liftOp i = TestData (Cont i)

And here's the error from ghci 7.4.2

src/Test.hs:13:26:
    Could not deduce (a' ~ Cont Int)
    from the context (Full (TestData a) Int a')
      bound by the type signature for
                 liftOp :: Full (TestData a) Int a' => Int -> TestData a a'
      at src/Test.hs:13:5-32
      a' is a rigid type variable bound by
         the type signature for
           liftOp :: Full (TestData a) Int a' => Int -> TestData a a'
         at src/Test.hs:13:5
    In the return type of a call of `Cont'
    In the first argument of `TestData', namely `(Cont i)'
    In the expression: TestData (Cont i)

Given that the TypeConv typeclass has a fundep that I read as: "Given repr and a, we can infer b" and provided an instance for Int, why can't ghc infer that a' ~ Cont Int ?

Is the first parameter of TestData just there to try to make the types work? I'm not sure what you're trying to achieve with it. Do you actually want this instance to create liftOp :: Int -> Cont Int but you had to wrap it in TestData? — AndrewC
That sort of type refinement simply isn't done with FunDeps. I don't know the details, but something would be hard to implement correctly in that. Use type families to do that stuff. — Daniel Fischer
@AndrewC: I just reduced my problem to a small test, so the superfluous type parm repr has no use here. The idea is that repr and a should both decide a' in TypeConv — Chetan

AndrewC AndrewC · Accepted Answer · 2012-09-25T23:21:57

If you want a type function, use Type Families - that's what they're for. Type Families are easy and do what you expect.

Often the reason that the compiler didn't infer your type is that you specified a functional dependency (logical relationship) rather than a function (calculating tool). Using fundeps is notoriously counter-intuitive, partly because you're doing logic programming at the type level whilst doing functional programming at the value level. Switch! Use functions at the type level, with the lovely Type Families extension. Comes with free lambda fridge magnet with just four tokens (p&p not included).

I'm not sure what you were trying to achieve, but here's an example - correct me if I'm heading in the wrong direction. You'll need

{-# LANGUAGE TypeFamilies #-}

Then we can define a class that includes a local type synonym, TypeConv which is our type function:

class Lift a where
    type TypeConv a
    liftOp :: a -> TypeConv a

And then we could make an instance

instance Lift Int where
    type TypeConv Int = TestData (Cont Int)
    liftOp i = TestData (Cont i)

and if we just want to wrap in Cont, we could do

instance Lift Integer where
    type TypeConv Integer = Cont Integer
    liftOp i = Cont i

and you can go crazy with

instance Lift Char where
    type TypeConv Char = [String]
    liftOp c = replicate 4 (replicate 5 c)

which lets you have

*Main> liftOp (5::Int)
TestData (Cont 5)

*Main> liftOp (5::Integer)
Cont 5

*Main> liftOp '5'
["55555","55555","55555","55555"]

Haskell: Why does GHC not infer type in this typeclass with fundeps?

2 Answers