"opt_univ fell into a hole"

[Conal Elliott]

Hi Simon. Thanks for the reply. My plugin appears to produce the HoleProv
indirectly (and to my surprise) while building a dictionary to satisfy a
given constraint, using mkNonCanonical and solveWanteds. I don't know why
solveWanteds produces a HoleProv in this case and not in the many others
I've tried. The constraint being solved in the example I included was
'HasRep (Vec ('S n_aCj7) (Key h_aCj6))', where HasRep is similar to Generic
(from GHC.Generics), and there is a HasRep instance for Vec ('S n x). Come
to think of it, the free type variable s_aD1S troubles me as well.

I'm not terribly confident in the code I use for constructing these
dictionaries (setting up and calling solveWanteds) during Core-to-Core
transformation. Do you know of any relevant example code, docs, etc?

Yes, I'm using -dcore-lint, as well explicitly linting each small
transformation step (while debugging). Doing so has been very helpful in
finding bugs quickly.

Cheers, - Conal

On Mon, Apr 4, 2016 at 2:48 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> Definitely a bug. All HoleProvs should be eliminated by the type checker.
>
>
>
> Did your plugin produce a HoleProv?  It definitely should not do so; see
> the notes with that constructor.
>
>
>
> Lint checks for this – did you run with –dcore-lint?
>
>
>
> Simon
>
>
>
> *From:* ghc-devs [mailto:ghc-devs-bounces at haskell.org] *On Behalf Of *Conal
> Elliott
> *Sent:* 02 April 2016 20:24
> *To:* ghc-devs at haskell.org
> *Subject:* "opt_univ fell into a hole"
>
>
>
> I'm getting the following error message from a GHC plugin I'm developing
> (note GHC version):
>
>     ghc-stage2: panic! (the 'impossible' happened)
>       (GHC version 8.1.20160307 for x86_64-apple-darwin):
>             opt_univ fell into a hole {aD1S}
>
> I don't get this error when compiling without my plugin, so I may well be
> violating a compiler invariant.
>
> Shortly before the error, the plugin produced the following dictionary
> expression, which does indeed contain a `UnivCo` with a `HoleProv`. The
> plugin does sometimes generate `UnivCo`s but not with `HoleProv`.
>
>     let {
>       $dHasRep_aD1T :: HasRep (Vec 'Z s_aD1R[fuv:0])
>       $dHasRep_aD1T = $fHasRepVec0 @ s_aD1R[fuv:0] } in
>     let {
>       $dHasRepZLVeczqZZZLKeyhZRZR_Ii5CR :: HasRep (Vec 'Z (Key h_aCnh))
>       $dHasRepZLVeczqZZZLKeyhZRZR_Ii5CR =
>         $dHasRep_aD1T
>         `cast` ((HasRep
>                    (Vec
>                       <'Z>_N
>                       (Sym U(hole:{aD1S}, Key h_aCnh,
> s_aD1R[fuv:0])_N))_N)_R
>                 :: HasRep (Vec 'Z s_aD1R[fuv:0])
>                    ~R# HasRep (Vec 'Z (Key h_aCnh))) } in
>     $dHasRepZLVeczqZZZLKeyhZRZR_Ii5CR
>
> Here, `Key` is a type family from `Data.Key` in the keys package, and
> `Vec` is a GADT of statically length-indexed lists.
>
> Suggestions?
>
> Thanks, - Conal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160404/59567b22/attachment.html>