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

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

...

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

Thanks, Richard! Unfortunately, zonkEvBinds is not exported from TcHsSyn. Do you think there's another route to zonking that could work for my circumstances? - Conal On Mon, Apr 4, 2016 at 2:00 PM, Richard Eisenberg wrote:

Can't say anything about the setup to use unsafePerformIO, but I can say that, yes, you need a zonk.

You may wish to read Note [What is zonking?] in TcMType. Running your bnds through a zonkEvBinds (using an emptyZonkEnv) should help.

Also, use TcMType.newWanted to make your CtWanted. As it stands, if predTy is an equality constraint, your CtWanted will be ill-formed, as all equality constraints should have HoleDests, not EvVarDests. Using TcMType.newWanted will simplify and improve your code.

I hope this helps, Richard

On Apr 4, 2016, at 7:16 PM, Conal Elliott 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 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 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

...

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

Thanks! Will do. On Tue, Apr 5, 2016 at 12:55 AM, Richard Eisenberg wrote:

No -- that's the one you want. Either wrap your EvBinds in some structure that you can zonk, or submit a patch exporting zonkEvBinds. :)

Richard

On Apr 4, 2016, at 11:56 PM, Conal Elliott wrote:

Thanks, Richard! Unfortunately, zonkEvBinds is not exported from TcHsSyn. Do you think there's another route to zonking that could work for my circumstances? - Conal

On Mon, Apr 4, 2016 at 2:00 PM, Richard Eisenberg wrote:

...

Can't say anything about the setup to use unsafePerformIO, but I can say that, yes, you need a zonk.

You may wish to read Note [What is zonking?] in TcMType. Running your bnds through a zonkEvBinds (using an emptyZonkEnv) should help.

Also, use TcMType.newWanted to make your CtWanted. As it stands, if predTy is an equality constraint, your CtWanted will be ill-formed, as all equality constraints should have HoleDests, not EvVarDests. Using TcMType.newWanted will simplify and improve your code.

I hope this helps, Richard

On Apr 4, 2016, at 7:16 PM, Conal Elliott 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 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 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@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@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 02 April 2016 20:24 *To:* ghc-devs@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs