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 ?

Answer 1

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"]