[Haskell-cafe] RE: [darcs-devel] advice on GADT type witnesses needed

[Simon Peyton-Jones]

I've improved the error message for this case. It was indeed bizarrely confusing.

Simon

| -----Original Message-----
| From: Ian Lynagh [mailto:igloo at earth.li]
| Sent: 15 June 2007 15:53
| To: Jason Dagit
| Cc: haskell-cafe at haskell.org; darcs-devel at darcs.net; Simon Peyton-Jones
| Subject: Re: [darcs-devel] advice on GADT type witnesses needed
|
| On Thu, Jun 14, 2007 at 08:27:36PM -0700, Jason Dagit wrote:
| > On 6/14/07, David Roundy <droundy at darcs.net> wrote:
| >
| > >src/Darcs/Patch/Show.lhs:50:0:
| > >    Quantified type variable `y' is unified with another quantified type
| > >    variable `x'
| > >    When trying to generalise the type inferred for `showPatch'
| > >      Signature type:     forall x y. Patch x y -> Doc
| > >      Type to generalise: Patch y y -> Doc
| > >    In the type signature for `showPatch'
| > >    When generalising the type(s) for showPatch, showComP, showSplit,
| > >                                      showConflicted, showNamed
| > >make: *** [src/Darcs/Patch/Show.o] Error 1
| > >
| > >The relevant code is
| > >
| > >showPatch :: Patch C(x,y) -> Doc
| > >showPatch (FP f AddFile) = showAddFile f
| > >...
| > >showPatch (Conflicted p ps) = showConflicted p ps
| > >
| > >and the trouble comes about because of (in Core.lhs)
| > >
| > >data Patch C(x,y) where
| > >    NamedP :: !PatchInfo -> ![PatchInfo] -> !(Patch C(x,y)) -> Patch C(x,y)
| > >...
| > >    Conflicted :: Patch C(a,b) -> FL Patch C(b,c) -> Patch C(c,c)
| > >
| >
| > I would like to add that I've tried (and failed) to construct a
| > minimal example that demonstrates the type check failure by simulating
| > the relevant code above.  This makes me wonder if the problem is not
| > in the obvious place(s).
|
| Here's one:
|
|     module Q where
|
|     data Foo x y where
|         Foo :: Foo a b -> Foo b c -> Foo c c
|
|     ------
|
|     module W where
|
|     import Q
|
|     wibble :: Foo a b -> String
|     wibble (Foo x y) = foo x y
|
|     foo :: Foo a b -> Foo b c -> String
|     foo x y = wibble x ++ wibble y
|
| 6.6 and 6.6.1 say:
|
| $ ghc -c Q.hs -fglasgow-exts
| $ ghc -c W.hs
|
| W.hs:7:0:
|     Quantified type variable `b' is unified with another quantified type variable `a'
|     When trying to generalise the type inferred for `wibble'
|       Signature type:     forall a b. Foo a b -> String
|       Type to generalise: Foo b b -> String
|     In the type signature for `wibble'
|     When generalising the type(s) for wibble, foo
| $ ghc -c W.hs -fglasgow-exts
| $
|
| i.e. you need to give the -fglasgow-exts flag when compiling W.hs.
| An {-# OPTIONS_GHC -fglasgow-exts #-} pragma in Show.lhs fixes the real
| thing too.
|
| The HEAD is the same, except the error is:
|
| W.hs:7:8:
|     GADT pattern match in non-rigid context for `Foo'
|       Tell GHC HQ if you'd like this to unify the context
|     In the pattern: Foo x y
|     In the definition of `wibble': wibble (Foo x y) = foo x y
|
| I suspect your problem in making a testcase was moving the GADT
| declaration into the same file as the function, and thus needing to
| compile it with -fglasgow-exts anyway.
|
| I'm not sure if GHC's behaviour is what is expected though; Simon?
|
|
| Thanks
| Ian