31 Jan 15:06 2013

## why GHC cannot infer type in this case?

Dmitry Kulagin <dmitry.kulagin <at> gmail.com>

2013-01-31 14:06:15 GMT

2013-01-31 14:06:15 GMT

Hi Cafe,

I try to implement little typed DSL with functions, but there is a problem: compiler is unable to infer type for my "functions". It seems that context is clear, but still GHC complains "Could not deduce...".

It is sad because without type inference the DSL will be very difficult to use.

Could someone explain me why this happens and how it can be avoided?

I use GHC 7.4.2

I tried to distill the code to show the problem (and full error message below it).

Thank you!

Dmitry

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

module TestExp where

-- Sequence of DSL's types to represent type of tuple

data TSeq where

TSeqEmpty :: TSeq

TSeqCons :: TypeExp -> TSeq -> TSeq

-- All types allowed in DSL

data TypeExp where

-- Primitive type

TInt16 :: TypeExp

-- Function type is built from types of arguments (TSeq) and type of result

TFun :: TSeq -> TypeExp -> TypeExp

-- Sequence of expressions to represent tuple

data Seq (t :: TSeq) where

SeqEmpty :: Seq TSeqEmpty

SeqCons :: Exp w -> Seq v -> Seq (TSeqCons w v)

data Exp (r :: TypeExp) where

Decl :: (Seq args -> Exp r) -> Exp (TFun args r)

Call :: Exp (TFun args r) -> Seq args -> Exp r

Int16 :: Int -> Exp TInt16

Add :: Exp TInt16 -> Exp TInt16 -> Exp TInt16

-- Assumed semantics: fun x = x + 2

-- The following line must be uncommented to compile without errors

-- fun :: Exp (TFun (TSeqCons TInt16 TSeqEmpty) TInt16)

fun = Decl $ \(SeqCons x SeqEmpty) -> Add (Int16 2) x

-- eval (Int16 x) = x

-- eval (Call (Decl f) seq) = eval (f seq)

-- eval (Add x y) = eval x + eval y

-- test = eval $ Call fun (SeqCons (Int16 3) SeqEmpty)

----------------- There is full error message: ----------------------------

TestExp.hs:30:53:

Could not deduce (w ~ 'TInt16)

from the context (args ~ TSeqCons w v)

bound by a pattern with constructor

SeqCons :: forall (w :: TypeExp) (v :: TSeq).

Exp w -> Seq v -> Seq (TSeqCons w v),

in a lambda abstraction

at TestExp.hs:30:16-33

or from (v ~ 'TSeqEmpty)

bound by a pattern with constructor

SeqEmpty :: Seq 'TSeqEmpty,

in a lambda abstraction

at TestExp.hs:30:26-33

`w' is a rigid type variable bound by

a pattern with constructor

SeqCons :: forall (w :: TypeExp) (v :: TSeq).

Exp w -> Seq v -> Seq (TSeqCons w v),

in a lambda abstraction

at TestExp.hs:30:16

Expected type: Exp 'TInt16

Actual type: Exp w

In the second argument of `Add', namely `x'

In the expression: Add (Int16 2) x

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe <at> haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe