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 <[email protected]> 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:[email protected]] *On Behalf Of *Conal > Elliott > *Sent:* 02 April 2016 20:24 > *To:* [email protected] > *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 >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
