GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-09T02:05:30Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24218QualifiedDo causes Core lint error (with my typechecker plugin)2024-03-09T02:05:30ZJaro ReindersQualifiedDo causes Core lint error (with my typechecker plugin)## Summary
I'm trying to develop a plugin that automatically solves transitivity of a type class that I've defined myself:
```haskell
type (<=) :: (Type -> Type) -> (Type -> Type) -> Constraint
class f <= g where
inj :: f x -> g x
-...## Summary
I'm trying to develop a plugin that automatically solves transitivity of a type class that I've defined myself:
```haskell
type (<=) :: (Type -> Type) -> (Type -> Type) -> Constraint
class f <= g where
inj :: f x -> g x
-- These are overlapping, but our plugin will resolve the overlap.
instance f <= f where
inj = id
instance forall f g h. (f <= g, g <= h) => f <= h where
inj = inj @g @h . inj @f @g
```
However, I'm running into an error that I cannot explain.
The error occurs in the `hsapply` function which is defined like this:
```haskell
hsapply :: Free MySig u (a -> b) -> Free MySig u a -> Free MySig u b
hsapply x y = Main.do
x' <- x
y' <- injfree y
Free (HsApply (inj x') y' (coerce Pure))
```
But the error disappears if I manually use my own `>>=`:
```haskell
hsapply :: Free MySig u (a -> b) -> Free MySig u a -> Free MySig u b
hsapply x y =
x Main.>>= \x' ->
injfree y Main.>>= \y' ->
Free (HsApply (inj x') y' (coerce Pure))
```
The type of my bind is:
```haskell
(>>=) :: UFunctor f => Free f u a -> (forall u'. (u <= u') => u' a -> Free f u' b) -> Free f u b
```
## Steps to reproduce
1. Clone https://github.com/noughtmare/transitive-constraint-plugin
2. Check out this problematic commit: `git checkout bb7f4cfec371f6053bb3f4d33130bc7a67166596`
3. Try to build the 'Free' example: `cabal build exe:free-example`
This produces a core lint error:
```
Out of scope: $d<=_a1fj :: u_a1eN <= u'_a1eW
[LclId]
```
The relevant snippet of Core is:
```haskell
>>=
@MySig
@u'_a1eW
@a_a1eO
@b_a1eP
$dUFunctor_a1f9
(injfree @u_a1eN @u'_a1eW @a_a1eO $d<=_a1fj y_aXB)
(\ (@(u'_a1fa :: * -> *)) ($d<=_a1fb :: u'_a1eW <= u'_a1fa) ->
let {
$d<=_a1fj :: u_a1eN <= u'_a1eW
[LclId]
$d<=_a1fj = $d<=_a1eX } in
```
Note how the `$d<=_a1fj` is referenced outside the let it is bound in.
But my plugin does not produce that reference as far as I can tell. My tracing ([source](https://github.com/noughtmare/transitive-constraint-plugin/blob/bb7f4cfec371f6053bb3f4d33130bc7a67166596/src/TransitiveConstraintPlugin.hs#L74)) shows that it only touches that name once and in that case it produces a contradiction:
```
contradiction: [W] $d<=_a1fj {0}:: u_a1eN[sk:1] <= u'_a1eW[sk:2] (CDictCan)
```
## Expected behavior
The `Free.hs` example should compile without issues.
## Environment
* GHC version used: 9.6.3Apoorv IngleApoorv Inglehttps://gitlab.haskell.org/ghc/ghc/-/issues/23905Provide a mechanism for backtracking in the constraint solver2023-09-04T19:24:08Zsheafsam.derbyshire@gmail.comProvide a mechanism for backtracking in the constraint solverConsider the following code in `GHC.Tc.Solver.disambGroup`:
```haskell
disambigGroup :: [Type] -> (TcTyVar, [Ct]) -> TcS Bool
disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= do { fake_ev_binds_var <- TcS.newTcEvBinds
...Consider the following code in `GHC.Tc.Solver.disambGroup`:
```haskell
disambigGroup :: [Type] -> (TcTyVar, [Ct]) -> TcS Bool
disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= do { fake_ev_binds_var <- TcS.newTcEvBinds
; tclvl <- TcS.getTcLevel
; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
; if success then
do { unifyTyVar the_tv default_ty; ... }
else ...
}
where
try_group
| Just subst <- mb_subst
= do { ..
; wanted_evs <- sequence [ newWantedNC loc rewriters pred'
| wanted <- wanteds
, CtWanted { ctev_pred = pred
, ctev_rewriters = rewriters }
<- return (ctEvidence wanted)
, let pred' = substTy subst pred ]
; fmap isEmptyWC $
solveSimpleWanteds $ listToBag $
map mkNonCanonical wanted_evs }
| otherwise
= return False
the_ty = mkTyVarTy the_tv
mb_subst = tcMatchTyKi the_ty default_ty
```
The way this works is that we have a set of Wanted constraints `wanteds` and a defaulting proposal `the_tv ~> default_ty`. We want to check whether substituting `the_tv ~> default_ty` allows us to solve all of the Wanted constraints. To do that, we apply the susbstitution and create new Wanteds, and call `solveSimpleWanteds` on these. Only when we get an empty set of residual constraints do we then decide that the defaulting assignment was valid, and thus only then do we perform the unification `the_tv := default_ty` (the call to `unifyTyVar`).
**However**, there is nothing that stops the solver from performing its own unifications. For example, after substituting, we could plausibly solve a class constraint using an instance whose superclass contains an equality. This equality could then cause unifications to happen, **before** we have decided we want to accept the defaulting proposal!
The problem is that we want to try a certain defaulting proposal, test it out with a run of the constraint solver, and backtrack if it turns out to not be fruitful. To achieve this, we could instead call the solver on a completely separate collection of type variables and constraints, so that any unifications that take place are isolated from the original type variables and constraints. Another option would be to have a way to "roll back" any unifications that took place.
Another application of this "roll-back" functionality is the [`if-instance` typechecker plugin](https://github.com/sheaf/if-instance). The way it works is that, to solve a constraint disjunction `ct1 || ct2`, it first tries to solve `ct1` (using `solveSimpleWanteds`); and if that fails it tries to solve `ct2`. The problem is that attempting to solve `ct1` might have caused unifications to take place, which we don't want. So again we should isolate the solver run to avoid it committing to certain undesirable unifications.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23832Extend defaulting plugin API to allow defaulting on multi-parameter type classes2023-09-01T09:47:55ZGergő ÉrdiExtend defaulting plugin API to allow defaulting on multi-parameter type classesCurrently, the defaulting plugin API matches exactly the signature of the built-in defaulting mechanism, where each type variable occuring in the `Wanteds` can be proposed to be defaulted to a priority list of types, one by one, with som...Currently, the defaulting plugin API matches exactly the signature of the built-in defaulting mechanism, where each type variable occuring in the `Wanteds` can be proposed to be defaulted to a priority list of types, one by one, with some extra constraints that need to hold after defaulting.
Since each new constraint is associated with a single defaultable type variable, this makes it impossible to propose defaults for multi-parameter typeclasses `C a b`, or even constraints with multiple as-yet-unsolved type variables`C (T a b)`.
However, it would not take much to extend the plugin API to support this use case. I have a prototype implementation at https://gitlab.haskell.org/cactus/ghc/-/commit/b73d407b20c2ba8c0792855b41d1b5dd5dc1aee5 that changes the API to this:
```
data DefaultingProposal
= DefaultingProposal
{ deProposalTyVars :: [TcTyVar]
-- ^ The type variable to default.
, deProposalCandidates :: [[Type]]
-- ^ Candidate types to default the type variable to.
, deProposalCts :: [Ct]
-- ^ The constraints against which defaults are checked.
}
```
The types could be a bit tighter, because basically we want a rectangle of proposal candidates (`all (equalLength deProposalTyVars) deProposalCandidates`), but I don't know how that's usually done in the GHC codebase so for the prototype this shall do.https://gitlab.haskell.org/ghc/ghc/-/issues/23763`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1:...2023-09-11T13:21:22ZMikolaj Konarski`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/):
* clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d
* `cabal build`
* you get
```
src/HordeAd/Core/As...Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/):
* clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d
* `cabal build`
* you get
```
src/HordeAd/Core/AstSimplify.hs:1192:9: error: [GHC-64725]
• Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1
• In the first argument of ‘($)’, namely ‘astTransposeS @zsuccPerm’
In the second argument of ‘($)’, namely
‘astTransposeS @zsuccPerm $ astReplicateS @n v’
In the second argument of ‘($)’, namely
‘trustMeThisIsAPermutation @zsuccPerm
$ astTransposeS @zsuccPerm $ astReplicateS @n v’
|
1192 | $ astTransposeS @zsuccPerm $ astReplicateS @n v
```
It works fine with GHC <= 9.6 and also after patching it in the following way:
https://github.com/Mikolaj/horde-ad/commit/0417f413051f1739fe32cfaf7869755276171449
My guess is that previously GHC could deduce:
OS.Rank zsuccPerm <= 1 + OS.Rank sh1
from (note that `sh2` that GHC invents here in just `zsuccPerm` -- this obfuscation in error messages is already reported in one of my older tickets)
OS.Rank zsuccPerm :~: 1 + OS.Rank perm
and
OS.Rank perm <= OS.Rank sh1
but now it can't.
The issue may be in GHC itself or in how plugin `GHC.TypeLits.Normalise` has been updated to 9.8.1-alpha1, but I doubt the latter, because it's been updated on head.hackage by people that know what they are doing.
I haven't tried with HEAD of the github repo of `GHC.TypeLits.Normalise` and GHC 9.6, but I don't think `GHC.TypeLits.Normalise` has been modified vs the version on Hackage (`GHC.TypeLits.KnownNat.Solver` has been, but it seem unrelated).
CC: @christiaanbhttps://gitlab.haskell.org/ghc/ghc/-/issues/23494"Deriving" plugins2023-06-13T18:04:00Zsheafsam.derbyshire@gmail.com"Deriving" pluginsI think it would be nice if the `deriving` infrastructure was extensible with plugins. This will probably need a GHC proposal in the end, but first I'd like to figure out how we would go about it.
I imagine it being a new deriving strat...I think it would be nice if the `deriving` infrastructure was extensible with plugins. This will probably need a GHC proposal in the end, but first I'd like to figure out how we would go about it.
I imagine it being a new deriving strategy which specifies a plugin name (module name):
```haskell
data P a = P3 a a a
deriving (Semigroup, Monoid)
plugin MyPlugin
```
In [Sam's plugin](https://github.com/sheaf/sams-plugin), I hijacked the `deriving via` mechanism to emulate this within a typechecking plugin:
```haskell
{-# OPTIONS_GHC -fplugin=Sam'sPlugin #-}
import Sam'sOptics
data D a = MkD { fld1 :: a, fld2 :: Int# }
deriving Sam'sOptics via Sam'sPlugin
```
This would create a collection of `HasField` instances:
```haskell
instance HasField "fld1" (D a) a
instance HasField "fld2" (D a) Int#
```
(for a custom `HasField` class which is representation-polymorphic).
The problem with this approach is that a typechecking plugin can't add instances to the instance environment without a lot of hacks. If we instead integrate it with `deriving`, then plugin-written instances will work as usual, without special logic.
One difficulty in the above example, which I believe is a key usability feature, is that we wrote a single deriving clause but it derived a bunch of instances. It would be quite onerous, for a record with many fields, to have to derive all of the `HasField` instances individually.https://gitlab.haskell.org/ghc/ghc/-/issues/23109Specialiser creates bogus specialisations2023-11-19T00:04:35ZMikolaj KonarskiSpecialiser creates bogus specialisationsSee also
* #21229
* #23445
* #23469
* #23866
* #23923 <--------- Apparently this is the one to fix first
## Original report
I'd like to ask for help in what is most probably a case of a bad port (by yours truly) of a typing plugin ...See also
* #21229
* #23445
* #23469
* #23866
* #23923 <--------- Apparently this is the one to fix first
## Original report
I'd like to ask for help in what is most probably a case of a bad port (by yours truly) of a typing plugin (GHC.TypeLits.Normalise) that fails in GHC 9.6.1, but worked fine in GHC 9.4.4 and 9.2.7 (and works fine in 9.6.1 with -O0). The typing breakage is described below. The bad port to GHC 9.6 is in https://github.com/clash-lang/ghc-tcplugins-extra/pull/24 and https://github.com/clash-lang/ghc-typelits-natnormalise/pull/72. I tried to follow the migration guide, but I didn't understand much and just randomly wibbled until it type-checked.
To reproduce, clone https://github.com/Mikolaj/horde-ad/tree/repro-rank-mismatch and run (the linters are included only to show they don't produce any info at all for the part of the codebase that is being compiled)
cabal test simplifiedOnlyTest --test-options='-p 3concatBuild' --allow-newer --enable-optimization --ghc-options='-dcore-lint -dstg-lint -dcmm-lint -dtag-inference-checks'
Normally it should pass fine, but instead you would be getting the following error
Exception: fromVector: rank mismatch (1,32)
where the value 32 comes from type variable `n`, from a *different* test than the one being run. If you change number 33 in this other test, you get a different error message. If you remove the other test, the error disappears. With -O0 and with older GHCs the problem does not appear. In larger versions of this reproducer, the error differed when run with profiling mode and without.
If it helps, I can try to minimize further, but the corruption is very fragile and tiny changes eliminate the error or at least change it to a form that is not as obviously wrong (does not mention a number from the code it should not depend on).
cc: @christiaanbMatthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21886Bundled clang does not handle long file paths on Windows2022-09-11T01:38:44ZChristiaan BaaijBundled clang does not handle long file paths on Windows## Summary
The `clang.exe` bundled with GHC 9.4.1-alpha3 does not handle long file paths on Windows.
This is a problem when working with type-checker plugins.
I discoved this while adding 9.4.1 support for one of our type-checker plugi...## Summary
The `clang.exe` bundled with GHC 9.4.1-alpha3 does not handle long file paths on Windows.
This is a problem when working with type-checker plugins.
I discoved this while adding 9.4.1 support for one of our type-checker plugins: https://github.com/clash-lang/ghc-typelits-natnormalise/pull/64
Running `cabal test` results in:
```
clang -cc1as: error: unable to open output file 'C:\\Users\\chris\\devel\\ghc-typelits-natnormalise\\dist-newstyle\\build\\x86_64-windows\\ghc-9.4.0.20220623\\ghc-typelits-natnormalise-0.7.7\\t\\test-ghc-typelits-natnormalise\\build\\test-ghc-typelits-natnormalise\\test-ghc-typelits-natnormalise-tmp\ErrorTests.o.tmp': 'No such file or directory'
<no location info>: error:
`clang.exe' failed in phase `Assembler'. (Exit code: 1)
```
## Steps to reproduce
```
mkdir -p C:/1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234/12345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890/12345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
echo "int main(){}" > main.c
C:\ghcup\ghc\9.4.1-alpha3\mingw\bin\clang.exe main.c -S -o C:/1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234/12345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890/12345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890/main.s
```
gives
```
error: unable to open output file
'C:/1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234/12345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890/123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678
'No such file or directory'
```
Enabling long paths as described in https://docs.microsoft.com/en-us/windows/win32/fileio/maximum-file-path-limitation?tabs=registry#enable-long-paths-in-windows-10-version-1607-and-later does not solve the issue.
## Expected behavior
Output the assembly of `main.c` to `main.s`.
## Environment
* GHC version used: 9.4.1-alpha3
Optional:
* Operating System: Windows 10 Pro 21H2 (build 19044.1826)
* System Architecture: x86_649.4.3Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/21427Irreducible givens hidden for TcPlugin2022-07-21T11:33:12ZPavol VargovčíkIrreducible givens hidden for TcPlugin## Motivation
Irreducible constraints could be often solved by TcPlugin, but irreducible givens are not accessible there.
## Proposal
Expose irreducible givens to TcPluginSolver.
~"typechecker plugins"## Motivation
Irreducible constraints could be often solved by TcPlugin, but irreducible givens are not accessible there.
## Proposal
Expose irreducible givens to TcPluginSolver.
~"typechecker plugins"https://gitlab.haskell.org/ghc/ghc/-/issues/20895TcPlugins: newWanted discards the source location2022-01-12T13:16:27Zsheafsam.derbyshire@gmail.comTcPlugins: newWanted discards the source locationWhen a plugin spins off a new Wanted constraint, using `newWanted`, based on a constraint it can simplify, the source location for the constraint is discarded.
This happens because we have:
```haskell
-- GHC.Tc.Plugin
newWanted :: CtLo...When a plugin spins off a new Wanted constraint, using `newWanted`, based on a constraint it can simplify, the source location for the constraint is discarded.
This happens because we have:
```haskell
-- GHC.Tc.Plugin
newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence
newWanted loc pty
= unsafeTcPluginTcM (TcM.newWanted (ctLocOrigin loc) Nothing pty)
-- GHC.Tc.Utils.TcMType
newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
newWanted orig t_or_k pty
= do loc <- getCtLocM orig t_or_k
d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole pty
else EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = d
, ctev_pred = pty
, ctev_nosh = WDeriv
, ctev_loc = loc }
-- GHC.Tc.Utils.Monad
getCtLocM :: CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM origin t_or_k
= do { env <- getLclEnv
; return (CtLoc { ctl_origin = origin
, ctl_env = env
, ctl_t_or_k = t_or_k
, ctl_depth = initialSubGoalDepth }) }
```
That is, starting with the `CtLoc` (which has the source span information we want), we keep only the `CtOrigin`, and discard the rest. The typechecker environment is then obtained from the monadic environment with `getLclEnv` in `getCtLocM`.
In practice, in a typechecking plugin, when one wants the emitted Wanted to have the same source location, one must wrap the `newWanted` call in `setCtLocM`. This sets the correct typechecker environment that to be retrieved by `getLcLEnv`.
If `GHC.Tc.Plugin.newWanted` is going to discard the local typechecking environment, then it should clearly indicate so in its type signature by taking a `CtOrigin` instead of a `CtLoc`.
@rae @nfrisby Do either of you have opinions on how to design the API to avoid this problem? Also tagging @edsko as he has been running into this issue.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/19981Test suite does not include any nontrivial type-checking plugins2022-02-24T14:43:46Zsheafsam.derbyshire@gmail.comTest suite does not include any nontrivial type-checking pluginsThe GHC test suite currently does not include any tests involving non-trivial type-checking plugins. All type-checking plugins tests use a simple stub plugin:
```haskell
thePlugin :: [CommandLineOption] -> TcPlugin
thePlugin opts = TcPl...The GHC test suite currently does not include any tests involving non-trivial type-checking plugins. All type-checking plugins tests use a simple stub plugin:
```haskell
thePlugin :: [CommandLineOption] -> TcPlugin
thePlugin opts = TcPlugin
{ tcPluginInit = return ()
, tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
, tcPluginStop = \_ -> return ()
}
```
On top of the obvious issue that we're not testing the solver part of the plugins, this also shields GHC developers from the consequences their changes might have on plugin authors. Having to update the plugins from the test suite to accommodate for changes in the internals of GHC would help GHC developers spell out possible migration strategies, much like head-hackage does today for other user-facing changes to GHC.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/19940tcLookup in plugins seems broken on HEAD2023-06-23T07:57:57Zsheafsam.derbyshire@gmail.comtcLookup in plugins seems broken on HEADThe operation of looking up names in a typechecker plugin seems to have been broken sometime recently. For instance:
```haskell
-- MyModule
type family MyFam a b where
-- MyPlugin
tcPluginInit :: TcPluginM ()
tcPluginInit = do
myMod...The operation of looking up names in a typechecker plugin seems to have been broken sometime recently. For instance:
```haskell
-- MyModule
type family MyFam a b where
-- MyPlugin
tcPluginInit :: TcPluginM ()
tcPluginInit = do
myModule <- findModule myPackage myModuleName
lookupResult <- tcLookupGlobal =<< lookupOrig myModule ( mkTcOcc "MyFam" )
pprPanic "Result was:" ( ppr lookupResult )
findModule :: String -> String -> TcPluginM Module
findModule pkg modName = do
findResult <- findImportedModule ( mkModuleName modName ) ( Just $ fsLit pkg )
case findResult of
Found _ res -> pure res
FoundMultiple _ -> error $ "MyPlugin: found multiple modules named " <> modName <> "."
_ -> error $ "MyPlugin: could not find any module named " <> modName <> "."
```
On GHC 9.2.1 (alpha1), I get the expected result:
```
GHC version 9.2.0.20210331:
Result was:
Type constructor `MyFam'
```
On GHC HEAD, when running in ghci I get:
```
GHC version 9.3.20210604:
Result was:
Identifier `disableBuffering'
```
and when compiling normally, I get:
```
GHC version 9.3.20210604:
Result was:
Identifier `plugin'
```
I have only checked 7a05185a and 79d12d34 and they both present the same issue. Note that this is on Windows 10 x64
(10.0.19041).
See here for full reproducer:
[tclookup.zip](/uploads/d1c32487021ec8e1c19d6b97b56f32ec/tclookup.zip)9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/19041Migration notes around !41492021-06-06T14:08:29ZRichard Eisenbergrae@richarde.devMigration notes around !4149Patch !4149 is a significant refactor of part of the constraint solver, removing the notion of flattening metavariables. This will have a direct downstream effect on any type-checker plugins. We should thus make a migration guide for dea...Patch !4149 is a significant refactor of part of the constraint solver, removing the notion of flattening metavariables. This will have a direct downstream effect on any type-checker plugins. We should thus make a migration guide for dealing with the change. @trac-sheaf and I emailed about building this together: @trac-sheaf has written type-checker plugins, and so knows the experience of a plugin author. I know the refactor and can guide the necessary changes. So let's build this migration guide together!https://gitlab.haskell.org/ghc/ghc/-/issues/16639enable typechecker plugins within tcCheckSatisfiability2020-05-03T10:06:43Znfrisbyenable typechecker plugins within tcCheckSatisfiability# Motivation
As of GHC 8.6.5, with my plugin enabled, the compiler awkwardly tells me a pattern is missing (non-exhaustive), **but** when I add the pattern it tells it is inaccessible.
My brief investigation suggests this is because th...# Motivation
As of GHC 8.6.5, with my plugin enabled, the compiler awkwardly tells me a pattern is missing (non-exhaustive), **but** when I add the pattern it tells it is inaccessible.
My brief investigation suggests this is because the pattern checker does not enable typechecker plugins, so it can't see the missing pattern is inaccessible, hence it warns non-exhaustive. But when that pattern is added, the typechecker plugin recognizes the contradiction when "simplifying Givens" (i.e. the formerly-missing pattern's context), and so it reports inaccessible. User catch 22.
# Example
In the following example. Suppose the plugin can see that `A B` and `B A` are impossible, but GHC alone cannot.
```
data AB where
A :: MutuallyExclusivePredicate_1of2 => AB
B :: MutuallyExclusivePredicate_2of2 => AB
```
The behavior on `f` is good and should not change.
```
{-# OPTIONS -fplugin=MyPlugin #-}
f :: AB -> ()
f B B = ()
f A B = () -- plugin reports contradiction when simplifying Givens, GHC reports inaccessible
f B A = () -- plugin reports contradiction when simplifying Givens, GHC reports inaccessible
```
But, the behavior for `g` is bad and should change; `g` should be warning free, but isn't.
```
{-# OPTIONS -fplugin=MyPlugin #-}
g :: AB -> ()
g A A = ()
g B B = ()
-- g A B = () -- bypassing plugin, pattern checker doesn't realize this is inaccessible; GHC reports non-exhaustive
-- g B A = () -- bypassing plugin, pattern checker doesn't realize this is inaccessible; GHC reports non-exhaustive
```
# Proposal
It seems the pattern checker should use typechecker plugins when checking (absent) patterns for satisfiability. Specifically, as of `aac18e9a08 - (tag: ghc-8.6.4-release) Bump to 8.6.4 (9 weeks ago) <Ben Gamari>`, my particular example seems fixed with just this trivial change to `DsMonad.initTcDsForSolver` plus necessary export & import list changes (the pattern checker calls `TcSimplify.tcCheckSatisfiability`, which calls `DsMonad.initTcDsForSolver`).
```
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 921276e4d8..72a1bdf124 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -247,6 +248,7 @@ initTcDsForSolver thing_inside
; liftIO $ initTc hsc_env HsSrcFile False mod loc $
updGblEnv (\tc_gbl -> tc_gbl { tcg_fam_inst_env = fam_inst_env }) $
+ TcRnDriver.withTcPlugins hsc_env $
thing_inside }
mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
```
I suspect it's significantly slower to use plugins for every pattern, so this would probably justify a new flag so a user can opt-out. (The flag should be implied by the presence of any typechecker plugins.)https://gitlab.haskell.org/ghc/ghc/-/issues/15745Panicking typechecker plugins2019-07-07T18:03:09ZPhil de JouxPanicking typechecker pluginsIf I use a typechecker plugin that fails then ghc panics and I'm asked to report a bug with GHC;
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64-apple-darwin):
Prelude.undefined
CallStack (from H...If I use a typechecker plugin that fails then ghc panics and I'm asked to report a bug with GHC;
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64-apple-darwin):
Prelude.undefined
CallStack (from HasCallStack):
error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
undefined, called at plugin/Undefined/Solve/Plugin.hs:14:39 in
undefined-solve-plugin-1.0.0.0-56evBabJYBHHTUlrE3HO5m:Undefined.Solve.Plugin
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Could we please say that it is the typechecker plugin that is panicking and ask for a bug report for the faulty typechecker, giving the issues URL for the plugin if we know it?
The following [undefined plugins](https://github.com/BlockScope/undefined-plugin) fail for init, solve and stop functions.
```haskell
module Undefined.Init.Plugin (plugin) where
import Plugins (Plugin(..), tcPlugin, defaultPlugin)
import TcRnTypes (TcPluginM, TcPluginResult(..), Ct, TcPlugin(..))
import GHC.TcPluginM.Extra (tracePlugin)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }
undefinedPlugin :: TcPlugin
undefinedPlugin = tracePlugin "undefined-init-plugin" $
TcPlugin
{ tcPluginInit = undefined
, tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
, tcPluginStop = const $ return ()
}
```
```haskell
module Undefined.Solve.Plugin (plugin) where
import Plugins (Plugin(..), tcPlugin, defaultPlugin)
import TcRnTypes (TcPluginM, TcPluginResult, Ct, TcPlugin(..))
import GHC.TcPluginM.Extra (tracePlugin)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }
undefinedPlugin :: TcPlugin
undefinedPlugin = tracePlugin "undefined-solve-plugin" $
TcPlugin
{ tcPluginInit = return ()
, tcPluginSolve = \_ _ _ _ -> undefined
, tcPluginStop = const $ return ()
}
```
```haskell
module Undefined.Stop.Plugin (plugin) where
import Plugins (Plugin(..), tcPlugin, defaultPlugin)
import TcRnTypes (TcPluginM, TcPluginResult(..), Ct, TcPlugin(..))
import GHC.TcPluginM.Extra (tracePlugin)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }
undefinedPlugin :: TcPlugin
undefinedPlugin = tracePlugin "undefined-stop-plugin" $
TcPlugin
{ tcPluginInit = return ()
, tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
, tcPluginStop = const $ undefined
}
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Panicking typechecker plugins","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"If I use a typechecker plugin that fails then ghc panics and I'm asked to report a bug with GHC;\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.2 for x86_64-apple-darwin):\r\n \tPrelude.undefined\r\n CallStack (from HasCallStack):\r\n error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err\r\n undefined, called at plugin/Undefined/Solve/Plugin.hs:14:39 in\r\n undefined-solve-plugin-1.0.0.0-56evBabJYBHHTUlrE3HO5m:Undefined.Solve.Plugin\r\n\r\n Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nCould we please say that it is the typechecker plugin that is panicking and ask for a bug report for the faulty typechecker, giving the issues URL for the plugin if we know it?\r\n\r\nThe following [https://github.com/BlockScope/undefined-plugin undefined plugins] fail for init, solve and stop functions.\r\n\r\n{{{\r\n#!haskell\r\nmodule Undefined.Init.Plugin (plugin) where\r\n\r\nimport Plugins (Plugin(..), tcPlugin, defaultPlugin)\r\nimport TcRnTypes (TcPluginM, TcPluginResult(..), Ct, TcPlugin(..))\r\nimport GHC.TcPluginM.Extra (tracePlugin)\r\n\r\nplugin :: Plugin\r\nplugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }\r\n\r\nundefinedPlugin :: TcPlugin\r\nundefinedPlugin = tracePlugin \"undefined-init-plugin\" $\r\n TcPlugin\r\n { tcPluginInit = undefined\r\n , tcPluginSolve = \\_ _ _ _ -> return $ TcPluginOk [] []\r\n , tcPluginStop = const $ return ()\r\n }\r\n}}}\r\n\r\n\r\n{{{\r\n#!haskell\r\nmodule Undefined.Solve.Plugin (plugin) where\r\n\r\nimport Plugins (Plugin(..), tcPlugin, defaultPlugin)\r\nimport TcRnTypes (TcPluginM, TcPluginResult, Ct, TcPlugin(..))\r\nimport GHC.TcPluginM.Extra (tracePlugin)\r\n\r\nplugin :: Plugin\r\nplugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }\r\n\r\nundefinedPlugin :: TcPlugin\r\nundefinedPlugin = tracePlugin \"undefined-solve-plugin\" $\r\n TcPlugin\r\n { tcPluginInit = return ()\r\n , tcPluginSolve = \\_ _ _ _ -> undefined\r\n , tcPluginStop = const $ return ()\r\n }\r\n}}}\r\n\r\n{{{\r\n#!haskell\r\nmodule Undefined.Stop.Plugin (plugin) where\r\n\r\nimport Plugins (Plugin(..), tcPlugin, defaultPlugin)\r\nimport TcRnTypes (TcPluginM, TcPluginResult(..), Ct, TcPlugin(..))\r\nimport GHC.TcPluginM.Extra (tracePlugin)\r\n\r\nplugin :: Plugin\r\nplugin = defaultPlugin { tcPlugin = const $ Just undefinedPlugin }\r\n\r\nundefinedPlugin :: TcPlugin\r\nundefinedPlugin = tracePlugin \"undefined-stop-plugin\" $\r\n TcPlugin\r\n { tcPluginInit = return ()\r\n , tcPluginSolve = \\_ _ _ _ -> return $ TcPluginOk [] []\r\n , tcPluginStop = const $ undefined\r\n }\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15633Type-checker plugins aren't loaded in GHCi 8.6.12019-07-07T18:03:39ZOleg GrenrusType-checker plugins aren't loaded in GHCi 8.6.1Type-Checker plugins seem to work in GHCi-8.4.3 https://gist.github.com/phadej/f2040eba327a88d3652cda021403f97f
However with GHC-8.6.1
The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180907
76a233143f1ec940f342ce3ce3af...Type-Checker plugins seem to work in GHCi-8.4.3 https://gist.github.com/phadej/f2040eba327a88d3652cda021403f97f
However with GHC-8.6.1
The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180907
76a233143f1ec940f342ce3ce3afaf306923b392 (which seems to be the last commit in 8.6 branch atm)
the plugins aren't loaded.
```
% ghci-8.6.1 -fplugin=ThereIsNoPlugin
GHCi, version 8.6.0.20180907: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ogre/.ghci
λ>
```
starts a session without a warning. 8.4.3 however fails:
```
% ghci-8.4.3 -fplugin=ThereIsNoPlugin
GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help
<command line>: Could not find module ‘ThereIsNoPlugin’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1-beta1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type-checker plugins aren't loaded in 8.6.1","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Type-Checker plugins seem to work in GHCi-8.4.3 https://gist.github.com/phadej/f2040eba327a88d3652cda021403f97f\r\n\r\nHowever with GHC-8.6.1\r\n\r\nThe Glorious Glasgow Haskell Compilation System, version 8.6.0.20180907\r\n76a233143f1ec940f342ce3ce3afaf306923b392 (which seems to be the last commit in 8.6 branch atm)\r\n\r\nthe plugins aren't loaded.\r\n\r\n{{{\r\n% ghci-8.6.1 -fplugin=ThereIsNoPlugin\r\nGHCi, version 8.6.0.20180907: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ogre/.ghci\r\nλ> \r\n}}}\r\n\r\nstarts a session without a warning. 8.4.3 however fails:\r\n\r\n{{{\r\n% ghci-8.4.3 -fplugin=ThereIsNoPlugin\r\nGHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help\r\n<command line>: Could not find module ‘ThereIsNoPlugin’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.3https://gitlab.haskell.org/ghc/ghc/-/issues/15322`KnownNat` does not imply `Typeable` any more when used with plugin2020-01-23T19:18:02ZDmitrii Kovanikov`KnownNat` does not imply `Typeable` any more when used with pluginI have the following Haskell code which uses `ghc-typelits-knownnat-0.5` package as a plugin:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin...I have the following Haskell code which uses `ghc-typelits-knownnat-0.5` package as a plugin:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Nats where
import Data.Proxy (Proxy (..))
import Data.Typeable (Typeable)
import GHC.TypeLits (KnownNat, type (+))
f :: forall n . (Typeable n, KnownNat n) => Proxy n -> ()
f _ = ()
f _ = f (Proxy :: Proxy (n + 1))
```
When I try to compile this code I observe the following error message:
```
• Could not deduce (Typeable (n + 1)) arising from a use of ‘f’
from the context: (Typeable n, KnownNat n)
bound by the type signature for:
f :: forall (n :: ghc-prim-0.5.2.0:GHC.Types.Nat).
(Typeable n, KnownNat n) =>
Proxy n -> ()
at src/Nats.hs:13:1-57
• In the expression: f (Proxy :: Proxy (n + 1))
In an equation for ‘f’: f _ = f (Proxy :: Proxy (n + 1))
|
15 | f _ = f (Proxy :: Proxy (n + 1))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This code works for both GHC-8.2.2 and GHC-8.0.2. I found similar ticket with exactly this problem but looks like this is broken again: #10348 (bug).
Originally reported at Github for `ghc-typelits-knownnat` package:
- https://github.com/clash-lang/ghc-typelits-knownnat/issues/21
`ghc-typelits-knownnat` package correctly infers `KnownNat (n + 1)` constraint so GHC should be able to infer `Typeable (n + 1)`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"`KnownNat` does not imply `Typeable` any more when used with plugin","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["typeable,knownnat"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I have the following Haskell code which uses `ghc-typelits-knownnat-0.5` package as a plugin:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\n{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}\r\n\r\nmodule Nats where\r\n\r\nimport Data.Proxy (Proxy (..))\r\nimport Data.Typeable (Typeable)\r\nimport GHC.TypeLits (KnownNat, type (+))\r\n\r\nf :: forall n . (Typeable n, KnownNat n) => Proxy n -> ()\r\nf _ = ()\r\nf _ = f (Proxy :: Proxy (n + 1))\r\n}}}\r\n\r\nWhen I try to compile this code I observe the following error message:\r\n\r\n{{{\r\n • Could not deduce (Typeable (n + 1)) arising from a use of ‘f’\r\n from the context: (Typeable n, KnownNat n)\r\n bound by the type signature for:\r\n f :: forall (n :: ghc-prim-0.5.2.0:GHC.Types.Nat).\r\n (Typeable n, KnownNat n) =>\r\n Proxy n -> ()\r\n at src/Nats.hs:13:1-57\r\n • In the expression: f (Proxy :: Proxy (n + 1))\r\n In an equation for ‘f’: f _ = f (Proxy :: Proxy (n + 1))\r\n |\r\n15 | f _ = f (Proxy :: Proxy (n + 1))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\n}}}\r\n\r\nThis code works for both GHC-8.2.2 and GHC-8.0.2. I found similar ticket with exactly this problem but looks like this is broken again: #10348 (bug).\r\n\r\nOriginally reported at Github for `ghc-typelits-knownnat` package:\r\n\r\n* https://github.com/clash-lang/ghc-typelits-knownnat/issues/21\r\n\r\n`ghc-typelits-knownnat` package correctly infers `KnownNat (n + 1)` constraint so GHC should be able to infer `Typeable (n + 1)`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15248Coercions from plugins cannot be stopped from floating out2020-06-15T03:39:49ZRichard Eisenbergrae@richarde.devCoercions from plugins cannot be stopped from floating outSuppose we have
```hs
type family (a :: Nat) <? (b :: Nat) :: Bool
```
that computes whether `a` is less than `b`, where a type checker plugin does the proof work. For some `a`, `b`, and `c`, if we assume `(a <? b) ~ True` and `(b <? c...Suppose we have
```hs
type family (a :: Nat) <? (b :: Nat) :: Bool
```
that computes whether `a` is less than `b`, where a type checker plugin does the proof work. For some `a`, `b`, and `c`, if we assume `(a <? b) ~ True` and `(b <? c) ~ True`, the plugin can prove `(a <? c) ~ True`. However, GHC currently provides no way for the plugin to indicate that the proof of `(a <? c) ~ True` depends on the assumptions. This means that the plugin-produced proof evidence could potentially float out of its desired context, inviting disaster.
In term of `Coercion`s, I propose that the `PluginProv` constructor of `UnivCoProvenance` be allowed to include a `TyCoVarSet` of "free variables" (that is, assumptions) in the proof. Computing the free variables of the enclosing `UnivCo` would returns these variables, too. It is, of course, up to the plugin to provide the right information here, but plugins generally have enough information to do this correctly (or, at least, to conservatively list all free variables of assumptions as free variables of the conclusion).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | --------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | dotwani@haverford.edu |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Coercions from plugins cannot be stopped from floating out","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["dotwani@haverford.edu"],"type":"Bug","description":"Suppose we have\r\n\r\n{{{#!hs\r\ntype family (a :: Nat) <? (b :: Nat) :: Bool\r\n}}}\r\n\r\nthat computes whether `a` is less than `b`, where a type checker plugin does the proof work. For some `a`, `b`, and `c`, if we assume `(a <? b) ~ True` and `(b <? c) ~ True`, the plugin can prove `(a <? c) ~ True`. However, GHC currently provides no way for the plugin to indicate that the proof of `(a <? c) ~ True` depends on the assumptions. This means that the plugin-produced proof evidence could potentially float out of its desired context, inviting disaster.\r\n\r\nIn term of `Coercion`s, I propose that the `PluginProv` constructor of `UnivCoProvenance` be allowed to include a `TyCoVarSet` of \"free variables\" (that is, assumptions) in the proof. Computing the free variables of the enclosing `UnivCo` would returns these variables, too. It is, of course, up to the plugin to provide the right information here, but plugins generally have enough information to do this correctly (or, at least, to conservatively list all free variables of assumptions as free variables of the conclusion).","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15147Type checker plugin receives Wanteds that are not completely unflattened2021-06-23T19:27:32ZnfrisbyType checker plugin receives Wanteds that are not completely unflattenedWith the following, a plugin will receive a wanted constraint that includes a `fsk` flattening skolem.
```
-- "Reduced" via the plugin
type family F u v where {}
type family G a b where {}
data D p where
DC :: (p ~ F x (G () ())) => ...With the following, a plugin will receive a wanted constraint that includes a `fsk` flattening skolem.
```
-- "Reduced" via the plugin
type family F u v where {}
type family G a b where {}
data D p where
DC :: (p ~ F x (G () ())) => D p
```
(Please ignore the apparent ambiguity regarding `x`; the goal is for the plugin to eliminate any ambiguity.)
A do-nothing plugin that merely logs its inputs gives the following for the ambiguity check on DC.
```
given
[G] $d~_a4oh {0}:: (p_a4o2[sk:2] :: *)
~ (p_a4o2[sk:2] :: *) (CDictCan)
[G] $d~~_a4oi {0}:: (p_a4o2[sk:2] :: *)
~~ (p_a4o2[sk:2] :: *) (CDictCan)
[G] co_a4od {0}:: (G () () :: *)
~# (fsk_a4oc[fsk:0] :: *) (CFunEqCan)
[G] co_a4of {0}:: (F x_a4o3[sk:2] fsk_a4oc[fsk:0] :: *)
~# (fsk_a4oe[fsk:0] :: *) (CFunEqCan)
[G] co_a4og {1}:: (fsk_a4oe[fsk:0] :: *)
~# (p_a4o2[sk:2] :: *) (CTyEqCan)
derived
wanted
[WD] hole{co_a4or} {3}:: (F x_a4o6[tau:2] fsk_a4oc[fsk:0] :: *)
~# (p_a4o2[sk:2] :: *) (CNonCanonical)
untouchables [fsk_a4oe[fsk:0], fsk_a4oc[fsk:0], x_a4o3[sk:2], p_a4o2[sk:2]]
```
Note the `fsk_a4oc[fsk:0]` tyvar in the Wanted constraint, which is why I'm opening this ticket. Its presence contradicts the "The wanteds will be unflattened and zonked" claim from https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker\#Callingpluginsfromthetypechecker section.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | adamgundry |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type checker plugin receives Wanteds that are not completely unflattened","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["checker","plugins","type"],"differentials":[],"test_case":"","architecture":"","cc":["adamgundry"],"type":"Bug","description":"With the following, a plugin will receive a wanted constraint that includes a `fsk` flattening skolem.\r\n\r\n{{{\r\n-- \"Reduced\" via the plugin\r\ntype family F u v where {}\r\ntype family G a b where {}\r\n\r\ndata D p where\r\n DC :: (p ~ F x (G () ())) => D p\r\n}}}\r\n\r\n(Please ignore the apparent ambiguity regarding `x`; the goal is for the plugin to eliminate any ambiguity.)\r\n\r\nA do-nothing plugin that merely logs its inputs gives the following for the ambiguity check on DC.\r\n\r\n{{{\r\ngiven\r\n [G] $d~_a4oh {0}:: (p_a4o2[sk:2] :: *)\r\n ~ (p_a4o2[sk:2] :: *) (CDictCan)\r\n [G] $d~~_a4oi {0}:: (p_a4o2[sk:2] :: *)\r\n ~~ (p_a4o2[sk:2] :: *) (CDictCan)\r\n [G] co_a4od {0}:: (G () () :: *)\r\n ~# (fsk_a4oc[fsk:0] :: *) (CFunEqCan)\r\n [G] co_a4of {0}:: (F x_a4o3[sk:2] fsk_a4oc[fsk:0] :: *)\r\n ~# (fsk_a4oe[fsk:0] :: *) (CFunEqCan)\r\n [G] co_a4og {1}:: (fsk_a4oe[fsk:0] :: *)\r\n ~# (p_a4o2[sk:2] :: *) (CTyEqCan)\r\nderived\r\nwanted\r\n [WD] hole{co_a4or} {3}:: (F x_a4o6[tau:2] fsk_a4oc[fsk:0] :: *)\r\n ~# (p_a4o2[sk:2] :: *) (CNonCanonical)\r\nuntouchables [fsk_a4oe[fsk:0], fsk_a4oc[fsk:0], x_a4o3[sk:2], p_a4o2[sk:2]]\r\n}}}\r\n\r\nNote the `fsk_a4oc[fsk:0]` tyvar in the Wanted constraint, which is why I'm opening this ticket. Its presence contradicts the \"The wanteds will be unflattened and zonked\" claim from https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Callingpluginsfromthetypechecker section.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14691Replace EvTerm with CoreExpr2019-07-07T18:15:59ZJoachim Breitnermail@joachim-breitner.deReplace EvTerm with CoreExprI asked
> I had some funky idea where a type checker plugin would have to \| synthesize code for a custom-solved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)
...I asked
> I had some funky idea where a type checker plugin would have to \| synthesize code for a custom-solved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)
>
> What would break if we had
>
> ```
> | EvExpr CoreExpr
> ```
>
> as an additional constructor there?
And Simon said
> This has come up before. I think that'd be a solid win.
>
> In fact, eliminate all the existing evidence constructors with "smart constructors" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.
>
> I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.
>
> You'd need to add `zonkCoreExpr` in place of `zonkEvTerm`.
>
> `evVarsOfTerm` is called quite a bit; you might want to cache the result in the `EvExpr` constructor.
This ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Replace EvTerm with CoreExpr","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"I asked\r\n\r\n> I had some funky idea where a type checker plugin would have to | synthesize code for a custom-solved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)\r\n>\r\n> What would break if we had\r\n> {{{\r\n> | EvExpr CoreExpr\r\n> }}}\r\n> as an additional constructor there?\r\n\r\nAnd Simon said\r\n\r\n> This has come up before. I think that'd be a solid win. \r\n> \r\n> In fact, eliminate all the existing evidence constructors with \"smart constructors\" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.\r\n> \r\n> I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.\r\n>\r\n> You'd need to add `zonkCoreExpr` in place of `zonkEvTerm`.\r\n>\r\n> `evVarsOfTerm` is called quite a bit; you might want to cache the result in the `EvExpr` constructor.\r\n\r\nThis ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12780Calling "do nothing" type checker plugin affects type checking when it shouldn't2020-10-13T17:53:57ZclintonCalling "do nothing" type checker plugin affects type checking when it shouldn'tThe following has been compiled against ghc version 8.1.20161022, my apologies if this bug has already been fixed.
The following program compiles fine:
```hs
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
...The following has been compiled against ghc version 8.1.20161022, my apologies if this bug has already been fixed.
The following program compiles fine:
```hs
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
main :: IO ()
main = return ()
type family F p = t | t -> p
type IsF p t = (C p, t ~ F p)
class C p where
f :: (IsF p t) => t
f = undefined
g :: (IsF p t) => t
g = f
```
But if we define a "do nothing" type checker plugin like so:
```hs
{-# OPTIONS_GHC -dynamic-too #-}
module MyPlugin (plugin) where
import Plugins (
Plugin(tcPlugin),
defaultPlugin, tcPlugin
)
import TcRnTypes (
TcPlugin(TcPlugin), tcPluginInit, tcPluginSolve, tcPluginStop,
TcPluginSolver,
TcPluginResult(TcPluginContradiction, TcPluginOk)
)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const (Just myPlugin) }
myPlugin :: TcPlugin
myPlugin =
TcPlugin
{
tcPluginInit = return (),
tcPluginSolve = const solver,
tcPluginStop = const (return ())
}
solver :: TcPluginSolver
solver _ _ _ = return $ TcPluginOk [] []
```
And call it from our original source file by adding:
```hs
{-# OPTIONS_GHC -fplugin MyPlugin #-}
```
We get the following error:
```
pluginbug.hs:18:5: error:
• Could not deduce (C p0, t ~ F p0) arising from a use of ‘f’
from the context: IsF p t
bound by the type signature for:
g :: IsF p t => t
at pluginbug.hs:17:1-19
The type variable ‘p0’ is ambiguous
Relevant bindings include g :: t (bound at pluginbug.hs:18:1)
• In the expression: f
In an equation for ‘g’: g = f
```
Note that not just calling my "do nothing" type checking plugin does this, to be sure, instead I called `ghc-typelits-natnormalise` like so:
```hs
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
```
And the same error results.
One solution is to remove `(C p)` from the `IsF` type declaration, and instead adding it to `g`s definition, like so:
```hs
--type IsF p t = (C p, t ~ F p)
type IsF p t = (t ~ F p)
--g :: (IsF p t) => t
g :: (C p, IsF p t) => t
```
In addition, either of the following two solutions will get the code to compile:
1. Replacing the reference to `IsF p t` in the class signature with `t ~ F p` like so:
```hs
-- f :: (IsF p t) => t
f :: (t ~ F p) => t
```
1. Alternatively, expanding out `IsF p t` in the signature of `g` as follows:
```hs
--g :: (IsF p t) => t
g :: (C p, t ~ F p) => t
```
Note that is we remove the class `C` entirely (making `f` an ordinary function) the bug disappears, but if instead replace the class with a constraint `C` like so:
```hs
type family C t :: Constraint
```
the bug still appears.
So it seems this bug needs four things to all occur for it to appear:
1. A type constraint synonym in the calling code.
1. A type constraint synonym in the called code.
1. The type constraint synonym to contain a class constraint, or at least a non-equality one.
1. A type checking plugin to be called.
Note that the error requires a type checking plugin to be called, if one does not override `defaultPlugin` like so:
```hs
plugin = defaultPlugin { tcPlugin = const (Just myPlugin) }
```
and instead just does:
```hs
plugin = defaultPlugin
```
then the issue will not occur.
So in summary, it seems that calling a type checking plugin somehow affects ordinary type checking in particular circumstances. I don't think this should happen.