GADT Type Checking GHC 6.10 versus older GHC

[Dominic Steinitz]

> In my case, we had rigid type signatures all over the place.  The
> wiki document says that the type must be rigid at the point of the
> match.  I guess that's what we were violating.  If the code I posted
> isn't supposed to type check then I would like to report, as user
> feedback, that GADTs have become unwieldy.

I'm now running into this problem big time on my existing test harness
(I'd previously checked the main code and that worked - see
http://www.haskell.org/pipermail/glasgow-haskell-users/2008-November/016160.html).

> 
> I grant that it's less convenient than one would like.  The
> difficulty is that GADTs get you into territory where it's easy to
> write programs that  have multiple *incomparable* types.   That is,
> there is no "best" type (unlike Hindley-Milner).  So we pretty much
> have to ask the programmer to express the type.
> 
> Once we are in that territory, we need to give simple rules that say
> when a type signature is needed.   I know that I have not yet found a
> way to express these rules -- perhaps GHC's users can help.  My
> initial shot is
> http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching
> 
> I couldn't figure out how to fix that code by just adding a type
> signature.

I've read this and I couldn't figure it out either. I've tried the
heuristic and it works fine for some cases but not others:

> arbitrarySeq :: Sequence a -> Gen RepSeqVal
> arbitrarySeq Nil =
>    return (RepSeqVal Nil Empty)
> arbitrarySeq (Cons (CTMandatory (NamedType n i t)) ts) =
>    do u <- arbitraryType t
>       us <- arbitrarySeq ts
>       case u of
>          RepTypeVal a v ->
>             case us of
>                RepSeqVal bs vs ->
>                   return (RepSeqVal (Cons (CTMandatory (NamedType n i a)) bs) (v:*:vs))


> QuickTest.lhs:240:13:
>     GADT pattern match in non-rigid context for `Nil'
>       Solution: add a type signature
>     In the pattern: Nil
>     In the definition of `arbitrarySeq':
>         arbitrarySeq Nil = return (RepSeqVal Nil Empty)

> *Rename> :t Nil
> Nil :: Sequence Nil

So this fixes the first case:

> arbitrarySeq :: Sequence a -> Gen RepSeqVal
> arbitrarySeq (Nil :: Sequence Nil) =
>    return (RepSeqVal Nil Empty)

But not the second case:

> QuickTest.lhs:242:14:
>     GADT pattern match in non-rigid context for `Cons'
>       Solution: add a type signature
>     In the pattern: Cons (CTMandatory (NamedType n i t)) ts
>     In the definition of `arbitrarySeq':
>         arbitrarySeq (Cons (CTMandatory (NamedType n i t)) ts)
>                        = do u <- arbitraryType t
>                             us <- arbitrarySeq ts
>                             case u of RepTypeVal a v -> ...

And now I'm stuck:

> *Rename> :t Cons
> Cons :: ComponentType a -> Sequence l -> Sequence (a :*: l)

What type should I give the Cons pattern? If I try the heuristic:

> arbitrarySeq ((Cons (CTMandatory (NamedType n i t)) ts) :: Int) =

the the compiler suggests

> QuickTest.lhs:242:14:
>     Couldn't match expected type `Sequence a'
>            against inferred type `Int'

but trying

> arbitrarySeq ((Cons (CTMandatory (NamedType n i t)) ts) :: Sequence a) =

gives

> QuickTest.lhs:242:68: Not in scope: type variable `a'


> 
> Did you try giving a type signature to the (entire) case expression,
> as I suggested?  That should do it.
> 

I'm not sure what this means or how to do it. Can you give an example or
is it buried in some earlier email? I will go and have another look.

> I urge you to consider designing a modified or new syntactic form for
> working with GADT pattern matches.  The quasi-dependent typing that
> GADTs give developers is very powerful and it would seem that GHC
> Haskell with GADTs is as close to dependent typing that developers
> writing "real-world" software can get.  I know of no other production
> ready compilers that provide dependent or close to dependent typing.
> Dependent typing seems to be a growing area of interest.  For these
> reasons I think it's important for GHC to focus on making them
> pleasanter to work with again; even if it means adding to the
> language again.
> 
> If I knew how to do that, I'd love to.  Here's one idea you might not
> like: restrict GADT matching to function definitions only (not case
> expressions), and require a type signature for such pattern matches.
> That wouldn't require adding new stuff.  But GHC's current story is a
> bit more flexible.
> 
> I also feel that the type errors given when working with existential
> types, especially GADTs with existentials, are confusing.  I think

I am using existential types to test GADT code. See
http://www.haskell.org/haskellwiki/QuickCheck_/_GADT which no longer
works with 6.10.1.

> mostly because the types of the sub-expressions in the program are
> not visible to the user.  More introspection into the inferred types
> would help users.  I have some ideas on how to improve this, what the
> output should look like and I would like to implement it too, but I
> haven't had a chance to start a prototype yet.
> 
> I agree they are confusing.  I always encourage people to suggest
> alternative wording for an error message that would make it less
> confusing (leaving aside how feasible or otherwise it'd be to
> generate such wording). So next time you are confused but figure it
> out, do suggest an alternative.
> 
> Thanks for helping.  You can't develop a good user interface without
> articulate and reflective users.  Thanks.
>