[darcs-devel] advice on GADT type witnesses needed

[Simon Peyton-Jones]

Good idea.  I'll improve the message by adding the suggestion to use a case expression instead.

Simon

| -----Original Message-----
| From: dagitj at gmail.com [mailto:dagitj at gmail.com] On Behalf Of Jason Dagit
| Sent: 21 June 2007 00:46
| To: Simon Peyton-Jones
| Cc: Ian Lynagh; haskell-cafe at haskell.org; darcs-devel at darcs.net
| Subject: Re: [darcs-devel] advice on GADT type witnesses needed
|
| On 6/20/07, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
| > I've improved the error message for this case. It was indeed bizarrely confusing.
|
| While we're on the subject of bizarrely confusing error messages :)
|
| I had some code like this:
| ...
|   where
|   MergeResult (_:>p2') (_:>p1' ) (_cp1 :\./:_cp2) = fancy_merge $ p1 :\./: p2
|
| and GHC gave me this error message:
|      My brain just exploded.
|      I can't handle pattern bindings for existentially-quantified constructors.
|
| Which is amusing, but it doesn't hint (enough) at the workaround,
| which appears to be using 'case' instead of let/where.  Any chance
| this could be improved to suggest the user tries switching to a case?
|
| I'm now using this code:
|   case fancy_merge $ p1 :\./: p2 of
|     MergeResult (_:>p2') (_:>p1' ) (_cp1 :\./:_cp2)
|
| Which seems to make it further with the type checking (my code is
| wrong, but at least now I get a normal error from ghc).
|
| Thanks,
| Jason
|
| >
| > 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
| >
| >