"opt_univ fell into a hole"

Mon Apr 4 18:34:50 UTC 2016

Oops. Just noticed an unfinished sentence. Meant to say "... where
runTcMUnsafe and runDsMUnsafe use unsafePerformIO (ouch) to construct
dictionary expressions in a 'built-in' rewrite rule". Of course, I'd love
to find a way not to need the unsafePerformIO.

On Mon, Apr 4, 2016 at 10:16 AM, Conal Elliott <conal at conal.net> wrote:

> Hi Richard. Thanks for the tips. I haven't learned about zonking, so it
> may well be what I'm missing here. I'm using some inherited code that
> includes the following line to get bindings then used with dsEvBinds and
> mkCoreLets to build an expression:
>
> >         (_wCs', bnds) <- second evBindMapBinds <$> runTcS (solveWanteds
> wCs)
>
> Should I be zonking in here somewhere?
>
> More context for this code, if helpful:
>
> > -- | Build a dictionary for the given
> > buildDictionary' :: HscEnv -> DynFlags -> ModGuts -> Id -> (Id,
> [CoreBind])
> > buildDictionary' env dflags guts evar =
> >     let (i, bs) = runTcMUnsafe env dflags guts $ do
> >         loc <- getCtLocM (GivenOrigin UnkSkol) Nothing
> >         let predTy = varType evar
> >             nonC = mkNonCanonical $
> >                      CtWanted { ctev_pred = predTy, ctev_dest =
> EvVarDest evar
> >                               , ctev_loc = loc }
> >             wCs = mkSimpleWC [cc_ev nonC]
> >         -- TODO: Make sure solveWanteds is the right function to call.
> >         (_wCs', bnds) <- second evBindMapBinds <$> runTcS (solveWanteds
> wCs)
> >         -- pprTrace "buildDictionary' _wCs'" (ppr _wCs') (return ())
> >         warnAllUnsolved _wCs'
> >         return (evar, bnds)
> >     in
> >       (i, runDsMUnsafe env dflags guts (dsEvBinds bs))
>
> where runTcMUnsafe and runDsMUnsafe use unsafePerformIO (ouch) to
>
> > runTcMUnsafe :: HscEnv -> DynFlags -> ModGuts -> TcM a -> a
> > runTcMUnsafe env dflags guts m = unsafePerformIO $ do
> >     -- What is the effect of HsSrcFile (should we be using something
> else?)
> >     -- What should the boolean flag be set to?
> >     (msgs, mr) <- initTcFromModGuts env guts HsSrcFile False m
> >     let showMsgs (warns, errs) = showSDoc dflags $ vcat
> >                                                  $    text "Errors:" :
> pprErrMsgBagWithLoc errs
> >                                                    ++ text "Warnings:" :
> pprErrMsgBagWithLoc warns
> >     maybe (fail $ showMsgs msgs) return mr
> >
> > -- TODO: Try initTcForLookup or initTcInteractive in place of
> initTcFromModGuts.
> > -- If successful, drop dflags and guts arguments.
> >
> > runDsMUnsafe :: HscEnv -> DynFlags -> ModGuts -> DsM a -> a
> > runDsMUnsafe env dflags guts = runTcMUnsafe env dflags guts . initDsTc
>
> and initTcFromModGuts is something I pulled in from HERMIT.
>
> Thanks and regards, - Conal
>
> On Mon, Apr 4, 2016 at 9:37 AM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
>
>> Coercion holes (the payload of a HoleProv) get created for all wanted
>> equality constraints (and for nothing else). If you're working over only
>> class dictionaries, you won't encounter holes. But my guess is that your
>> HasRep somehow induces a wanted equality. If the solver fills the hole --
>> as it should if the equality is solvable -- then you may just need to zonk
>> it properly. zonkCoHole does the job, but this should be called from
>> zonkTcTypeToType, which I imagine you're already doing.
>>
>> I hope this helps,
>> Richard
>>
>> On Apr 4, 2016, at 6:21 PM, Conal Elliott <conal at conal.net> wrote:
>>
>> 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
>>>
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160404/5d6c188c/attachment.html>