why GHC cannot infer type in this case?
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
Hi Dmitry.
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?
Pattern matches on GADT generally require type information. Type inference in such a case is tricky. GADTs are so powerful that in many cases, there's no unique best type to infer. As a contrived example, consider this datatype and function:
data X :: * -> * where C :: Int -> X Int D :: X a
f (C n) = [n] f D = []
What should GHC infer for f? Both
f :: X a -> [Int] f :: X a -> [a]
are reasonable choices, but without further information about the context, it's impossible to say which one of the two is better. It is theoretically possible to be more clever than GHC is and infer the types of GADT pattern matches in some cases. However, it is (A) a lot of work to implement and maintain that cleverness, and (B) it is then very difficult to describe when exactly a type signature is required and when it isn't. So GHC adopts the simpler approach and requires type information for all GADT pattern matches, which is a simple and predictable rule. How to prevent such errors in general is difficult to say. In your particular case, there might be an option, though. If you additionally use TypeFamilies and FlexibleInstances, you can define:
class MkDecl d where type MkDeclSeq d :: TSeq type MkDeclRes d :: TypeExp decl' :: d -> Seq (MkDeclSeq d) -> Exp (MkDeclRes d)
instance MkDecl (Exp r) where type MkDeclSeq (Exp r) = TSeqEmpty type MkDeclRes (Exp r) = r decl' e = \ SeqEmpty -> e
instance MkDecl d => MkDecl (Exp w -> d) where type MkDeclSeq (Exp w -> d) = TSeqCons w (MkDeclSeq d) type MkDeclRes (Exp w -> d) = MkDeclRes d decl' f = \ (SeqCons x xs) -> decl' (f x) xs
decl :: MkDecl d => d -> Exp (TFun (MkDeclSeq d) (MkDeclRes d)) decl d = Decl (decl' d)
fun = decl $ \ x -> Add (Int16 2) x
The idea here is to avoid pattern matching on the GADT, and instead use an ordinary Haskell function as an argument to the "decl" smart constructor. We use the type class and two type families to pack that function (with as many arguments as it has) into the type-level list and wrap it all up in the original "Decl". This works because on the outside, no GADT pattern matches are involved, and within the type class instances, the necessary type information is present. This is certainly harder to understand than your original version. On the other hand, it's actually easier to use. (It's entirely possible that my code can be simplified further. I haven't thought about this for very long ...) Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
Andres, thank you!
Your response is really helpful. I will try to adopt your suggestion.
Thank again!
Dmitry
On Thu, Jan 31, 2013 at 7:27 PM, Andres Löh
Hi Dmitry.
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?
Pattern matches on GADT generally require type information. Type inference in such a case is tricky. GADTs are so powerful that in many cases, there's no unique best type to infer.
As a contrived example, consider this datatype and function:
data X :: * -> * where C :: Int -> X Int D :: X a
f (C n) = [n] f D = []
What should GHC infer for f? Both
f :: X a -> [Int] f :: X a -> [a]
are reasonable choices, but without further information about the context, it's impossible to say which one of the two is better.
It is theoretically possible to be more clever than GHC is and infer the types of GADT pattern matches in some cases. However, it is (A) a lot of work to implement and maintain that cleverness, and (B) it is then very difficult to describe when exactly a type signature is required and when it isn't. So GHC adopts the simpler approach and requires type information for all GADT pattern matches, which is a simple and predictable rule.
How to prevent such errors in general is difficult to say. In your particular case, there might be an option, though. If you additionally use TypeFamilies and FlexibleInstances, you can define:
class MkDecl d where type MkDeclSeq d :: TSeq type MkDeclRes d :: TypeExp decl' :: d -> Seq (MkDeclSeq d) -> Exp (MkDeclRes d)
instance MkDecl (Exp r) where type MkDeclSeq (Exp r) = TSeqEmpty type MkDeclRes (Exp r) = r decl' e = \ SeqEmpty -> e
instance MkDecl d => MkDecl (Exp w -> d) where type MkDeclSeq (Exp w -> d) = TSeqCons w (MkDeclSeq d) type MkDeclRes (Exp w -> d) = MkDeclRes d decl' f = \ (SeqCons x xs) -> decl' (f x) xs
decl :: MkDecl d => d -> Exp (TFun (MkDeclSeq d) (MkDeclRes d)) decl d = Decl (decl' d)
fun = decl $ \ x -> Add (Int16 2) x
The idea here is to avoid pattern matching on the GADT, and instead use an ordinary Haskell function as an argument to the "decl" smart constructor. We use the type class and two type families to pack that function (with as many arguments as it has) into the type-level list and wrap it all up in the original "Decl". This works because on the outside, no GADT pattern matches are involved, and within the type class instances, the necessary type information is present.
This is certainly harder to understand than your original version. On the other hand, it's actually easier to use.
(It's entirely possible that my code can be simplified further. I haven't thought about this for very long ...)
Cheers, Andres
-- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com
participants (2)
-
Andres Löh -
Dmitry Kulagin