[Haskell-cafe] why GHC cannot infer type in this case?
Dmitry Kulagin
dmitry.kulagin at gmail.com
Thu Jan 31 15:06:15 CET 2013
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130131/23880d5e/attachment.htm>
More information about the Haskell-Cafe
mailing list