GADT problems

Mitchell, Neil neil.mitchell.2 at credit-suisse.com
Mon Sep 15 05:58:10 EDT 2008


Hi Simon,

> | op (Foo GadtValue :: Foo) = () :: ()
> 
> The thing is that GHC doesn't know the result type of the 
> match *at the match point*.  Suppose you had written
> 
>         op (Foo GadtValue :: Foo) = id (() :: ()) or
>         op (Foo GadtValue :: Foo) = if blah then () :: () else () or
>         op (Foo GadtValue :: Foo) = let x = blah in () :: ()
> 
> The signature is too far "inside".   We need to know it from 
> "outside".

Ah, this is the crucial bit I've been misunderstanding! Instinctively it
feels that when a GADT can't type check I should be annotating the GADT
part - but that's not the case, I should be annotating the expression
containing both the GADT match and its right-hand side. I think the way
the error message is formatted (add a type signature, followed by giving
the local pattern) seems to hint at this. With this insight I've managed
to fix up all the real problems I was experiencing.

My general method for solving these problems was to find an expression
or statement that enclosed both the left and right hand sides, and add
":: Int" to it. I then recompiled and got an error message saying it
couldn't match Int with <something>. I then replaced Int with
<something> and it worked. It seems surprising that the compiler can't
jump through those hoops for me, but I realise my particular cases may
be uncommon or the complexity may be too great. A nice addition to the
error message would be hinting at where the type signature should go, if
it can reasonably be determined.

> | I think this is the underlying problem I'm getting. For things like 
> | list-comps and cases I don't seem to be able to find any 
> combination 
> | of annotations that works, but that is because I'm not 
> using top-level 
> | annotations.
> 
> Perhaps you can give an example that shows your difficulty?

The following is a fake example I was playing with:

{-# LANGUAGE GADTs, ScopedTypeVariables #-}
module Test where

data E x = E x

data Foo a where
  Foo :: Gadt a -> Foo a

data Gadt a where
  GadtValue :: a -> Gadt (E a)

g :: [()]
g = [() | Foo (GadtValue _) <- undefined] :: [()]

I couldn't figure out how to supply enough annotations to allow the code
to work.

Thanks

Neil

==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================



More information about the Glasgow-haskell-users mailing list