<div dir="ltr">Hi Cafe,<div><br></div><div style>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...".</div>
<div style>It is sad because without type inference the DSL will be very difficult to use. </div><div style>Could someone explain me why this happens and how it can be avoided?</div><div style><br></div><div>I use GHC 7.4.2</div>
<div style>I tried to distill the code to show the problem (and full error message below it).<br></div><div style><br></div><div style>Thank you!</div><div style>Dmitry</div><div style><br></div><div style><div>{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}</div>
<div>module TestExp where</div><div><br></div><div>-- Sequence of DSL's types to represent type of tuple</div><div>data TSeq where</div><div> TSeqEmpty :: TSeq</div><div> TSeqCons :: TypeExp -> TSeq -> TSeq</div>
<div><br></div><div>-- All types allowed in DSL</div><div>data TypeExp where</div><div> -- Primitive type</div><div> TInt16 :: TypeExp</div><div> -- Function type is built from types of arguments (TSeq) and type of result</div>
<div> TFun :: TSeq -> TypeExp -> TypeExp</div><div><br></div><div>-- Sequence of expressions to represent tuple</div><div>data Seq (t :: TSeq) where</div><div> SeqEmpty :: Seq TSeqEmpty</div><div> SeqCons :: Exp w -> Seq v -> Seq (TSeqCons w v)</div>
<div><br></div><div>data Exp (r :: TypeExp) where</div><div> Decl :: (Seq args -> Exp r) -> Exp (TFun args r)</div><div> Call :: Exp (TFun args r) -> Seq args -> Exp r</div><div> Int16 :: Int -> Exp TInt16</div>
<div> Add :: Exp TInt16 -> Exp TInt16 -> Exp TInt16</div><div><br></div><div>-- Assumed semantics: fun x = x + 2</div><div>-- The following line must be uncommented to compile without errors<br></div><div>-- fun :: Exp (TFun (TSeqCons TInt16 TSeqEmpty) TInt16)</div>
<div>fun = Decl $ \(SeqCons x SeqEmpty) -> Add (Int16 2) x</div><div><br></div><div><br></div><div>-- eval (Int16 x) = x</div><div>-- eval (Call (Decl f) seq) = eval (f seq)</div><div>-- eval (Add x y) = eval x + eval y</div>
<div><br></div><div>-- test = eval $ Call fun (SeqCons (Int16 3) SeqEmpty)</div><div><br></div><div style>----------------- There is full error message: ----------------------------</div><div style><div><div>TestExp.hs:30:53:</div>
<div> Could not deduce (w ~ 'TInt16)</div><div> from the context (args ~ TSeqCons w v)</div><div> bound by a pattern with constructor</div><div> SeqCons :: forall (w :: TypeExp) (v :: TSeq).</div>
<div> Exp w -> Seq v -> Seq (TSeqCons w v),</div><div> in a lambda abstraction</div><div> at TestExp.hs:30:16-33</div><div> or from (v ~ 'TSeqEmpty)</div><div> bound by a pattern with constructor</div>
<div> SeqEmpty :: Seq 'TSeqEmpty,</div><div> in a lambda abstraction</div><div> at TestExp.hs:30:26-33</div><div> `w' is a rigid type variable bound by</div><div> a pattern with constructor</div>
<div> SeqCons :: forall (w :: TypeExp) (v :: TSeq).</div><div> Exp w -> Seq v -> Seq (TSeqCons w v),</div><div> in a lambda abstraction</div><div> at TestExp.hs:30:16</div>
<div> Expected type: Exp 'TInt16</div><div> Actual type: Exp w</div><div> In the second argument of `Add', namely `x'</div><div> In the expression: Add (Int16 2) x</div></div><div><br></div></div>
<div><br></div></div></div>