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