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

[Jason Dagit]

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
>
>