[Haskell-cafe] why GHC cannot infer type in this case?

[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