GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-06-13T18:04:00Zhttps://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/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/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/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/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/23109Specialiser creates bogus specialisations2024-03-29T12:29:36ZMikolaj KonarskiSpecialiser creates bogus specialisationsSee also
* #21229
* #23445
* #23469
* #23866
* #23923 <--------- Apparently this is the one to fix first
* #24606
## 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 typin...See also
* #21229
* #23445
* #23469
* #23866
* #23923 <--------- Apparently this is the one to fix first
* #24606
## 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/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/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/11457Run type-checker plugins before GHC's solver2020-01-23T19:37:33ZEric SeidelRun type-checker plugins before GHC's solverHere's an odd use-case for type-checker plugins: rejecting *valid* programs that the user doesn't like, for example, programs that use a class instance with confusing behavior (like the functor/traversable instances on tuples).
Unfortun...Here's an odd use-case for type-checker plugins: rejecting *valid* programs that the user doesn't like, for example, programs that use a class instance with confusing behavior (like the functor/traversable instances on tuples).
Unfortunately, we can't write such a plugin at the moment because GHC runs its own solver first, and will (I think) discharge any dictionary constraints before the plugin can run. If instead we run the plugins first, a plugin could mark undesired instances as insoluble.
See the discussion at http://mail.haskell.org/pipermail/libraries/2016-January/026602.html for the original motivation.
Thoughts?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | adamgundry, diatchki |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Run type-checker plugins before GHC's solver","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["plugin"],"differentials":[],"test_case":"","architecture":"","cc":["adamgundry","diatchki"],"type":"FeatureRequest","description":"Here's an odd use-case for type-checker plugins: rejecting ''valid'' programs that the user doesn't like, for example, programs that use a class instance with confusing behavior (like the functor/traversable instances on tuples).\r\n\r\nUnfortunately, we can't write such a plugin at the moment because GHC runs its own solver first, and will (I think) discharge any dictionary constraints before the plugin can run. If instead we run the plugins first, a plugin could mark undesired instances as insoluble.\r\n\r\nSee the discussion at http://mail.haskell.org/pipermail/libraries/2016-January/026602.html for the original motivation.\r\n\r\nThoughts?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11435Evidence from TC Plugin triggers core-lint warning2019-07-07T18:30:25ZjbrackerEvidence from TC Plugin triggers core-lint warningThe attached plugin and program produce a core-lint warning that refers to evidence the plugin did not produce.
## High-Level description of what the plugin does and what happens
'flatFilter' produces the following ambiguous wanted con...The attached plugin and program produce a core-lint warning that refers to evidence the plugin did not produce.
## High-Level description of what the plugin does and what happens
'flatFilter' produces the following ambiguous wanted constraints:
```
Polymonad (Reader '["thres" :-> Int]) n (Reader '["thres" :-> Int]) (CNonCanonical)
Polymonad (Reader '["thres" :-> Int]) m n (CNonCanonical)
Polymonad Identity Identity m
```
To solve these the plugin does the following:
1. It produces two type equality constraints:
`
n ~ Identity (CNonCanonical)
m ~ Reader '["thres" :-> Int] (CNonCanonical)
`
1. As a result of these equality constraints the GHC constraint solver creates
the following wanted constraint:
> `
> Polymonad (Reader '["thres" :-> Int]) Identity (Reader '["thres" :-> Int]) (CNonCanonical)
> `
> GHCs constraint solver can not pick an instance because several instances overlap:
```
P.Monad f => Polymonad f Identity f
( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m)) => Polymonad (m (f :: [*])) Identity (m (f :: [*]))
```
> By trying to produce evidence for either of these instances the plugin determines
> that only the second instance is actually applicable and therefore selects it and produces
> evidence.
With this the constraints are solved and the type checking/constraint solving stage
is done. During core linting we get the following error:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
[RHS of ds_a66V :: (Set '["thres" :-> Int], Set (Unit Reader))]
Bad getNth:
Nth:0
(Nth:2
(Sub (Sym (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N <'[]>_N))
; (Inv
<Reader>_N <'["thres" :-> Int]>_N (Sym TFCo:R:Unit[]Reader[0]))_R
; Sub
(TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N <Unit Reader>_N)))
Split '["thres" :-> Int] '[] (Union '["thres" :-> Int] '[])
Split
'["thres" :-> Int]
(Unit Reader)
(Union '["thres" :-> Int] (Unit Reader))
```
As can be seen in the plugin \[Check for 'Nth' constructor\] the evidence produced by the plugin does
not contain the 'Nth' constructor for coercions/evidence anywhere. Thus, the
produced evidence seems to trigger GHC to produce these 'bad' coercions/evidence
somewhere.
## Building the Example
The example should be self-contained and reproduces the error whenever you try to build it. You can find it here or in the attachment:
https://github.com/jbracker/polymonad-plugin/tree/master/examples/core-error
You just have to download the three files and run "cabal install" to reproduce the error. There is a high-level explanation of
what is going on above and in the 'Main.hs' from line 83. The plugin 'MinimalPlugin.hs' is still around 600 lines long, but I have added a lot of comments to make it comprehensible.
I suppose the most interesting part is the production of evidence in 'MinimalPlugin.hs' from line 198. I have added checks to see if the evidence I produce contains the 'Nth' constructors the core-lint warning refers to in line 130 and 556 of the plugin, but the evidence produced does not contain them. So somehow the evidence triggers GHC to produce evidence that the core-linter warns about.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.2 |
| 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":"Evidence from TC Plugin triggers core-lint warning","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":["core-lint","evidence","plugin","type-checker","warning"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The attached plugin and program produce a core-lint warning that refers to evidence the plugin did not produce.\r\n\r\n== High-Level description of what the plugin does and what happens\r\n\r\n'flatFilter' produces the following ambiguous wanted constraints:\r\n{{{\r\n Polymonad (Reader '[\"thres\" :-> Int]) n (Reader '[\"thres\" :-> Int]) (CNonCanonical)\r\n Polymonad (Reader '[\"thres\" :-> Int]) m n (CNonCanonical)\r\n Polymonad Identity Identity m\r\n}}}\r\nTo solve these the plugin does the following:\r\n1. It produces two type equality constraints:\r\n {{{\r\n n ~ Identity (CNonCanonical)\r\n m ~ Reader '[\"thres\" :-> Int] (CNonCanonical)\r\n }}}\r\n2. As a result of these equality constraints the GHC constraint solver creates \r\n the following wanted constraint:\r\n {{{\r\n Polymonad (Reader '[\"thres\" :-> Int]) Identity (Reader '[\"thres\" :-> Int]) (CNonCanonical)\r\n }}}\r\n GHCs constraint solver can not pick an instance because several instances overlap:\r\n{{{\r\nP.Monad f => Polymonad f Identity f\r\n( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m)) => Polymonad (m (f :: [*])) Identity (m (f :: [*]))\r\n}}}\r\n By trying to produce evidence for either of these instances the plugin determines \r\n that only the second instance is actually applicable and therefore selects it and produces \r\n evidence.\r\nWith this the constraints are solved and the type checking/constraint solving stage\r\nis done. During core linting we get the following error:\r\n{{{\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: Warning:\r\n [RHS of ds_a66V :: (Set '[\"thres\" :-> Int], Set (Unit Reader))]\r\n Bad getNth:\r\n Nth:0\r\n (Nth:2\r\n (Sub (Sym (TFCo:R:Inv[]Readerfg[0] <'[\"thres\" :-> Int]>_N <'[]>_N))\r\n ; (Inv\r\n <Reader>_N <'[\"thres\" :-> Int]>_N (Sym TFCo:R:Unit[]Reader[0]))_R\r\n ; Sub\r\n (TFCo:R:Inv[]Readerfg[0] <'[\"thres\" :-> Int]>_N <Unit Reader>_N)))\r\n Split '[\"thres\" :-> Int] '[] (Union '[\"thres\" :-> Int] '[])\r\n Split\r\n '[\"thres\" :-> Int]\r\n (Unit Reader)\r\n (Union '[\"thres\" :-> Int] (Unit Reader))\r\n}}}\r\nAs can be seen in the plugin [Check for 'Nth' constructor] the evidence produced by the plugin does\r\nnot contain the 'Nth' constructor for coercions/evidence anywhere. Thus, the \r\nproduced evidence seems to trigger GHC to produce these 'bad' coercions/evidence \r\nsomewhere.\r\n\r\n== Building the Example\r\n\r\nThe example should be self-contained and reproduces the error whenever you try to build it. You can find it here or in the attachment:\r\nhttps://github.com/jbracker/polymonad-plugin/tree/master/examples/core-error\r\n\r\nYou just have to download the three files and run \"cabal install\" to reproduce the error. There is a high-level explanation of \r\nwhat is going on above and in the 'Main.hs' from line 83. The plugin 'MinimalPlugin.hs' is still around 600 lines long, but I have added a lot of comments to make it comprehensible.\r\n\r\nI suppose the most interesting part is the production of evidence in 'MinimalPlugin.hs' from line 198. I have added checks to see if the evidence I produce contains the 'Nth' constructors the core-lint warning refers to in line 130 and 556 of the plugin, but the evidence produced does not contain them. So somehow the evidence triggers GHC to produce evidence that the core-linter warns about.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10077Providing type checker plugin on command line results in false cyclic import ...2019-07-07T18:37:39ZjbrackerProviding type checker plugin on command line results in false cyclic import errorI am playing around with the new type checker plugins using the current development branch of GHC. When I supply the plugin module to GHC through the command line I get a cyclic import error message, which I think is false. If I supply t...I am playing around with the new type checker plugins using the current development branch of GHC. When I supply the plugin module to GHC through the command line I get a cyclic import error message, which I think is false. If I supply the same plugin module using a pragma I do not get an error message.
### Minimal Example (Command Line)
`MyPlugin.hs`:
```hs
module MyPlugin ( plugin ) where
import Plugins ( Plugin, defaultPlugin )
plugin :: Plugin
plugin = defaultPlugin
```
`Test.hs`:
```hs
module Test where
main :: IO ()
main = return ()
```
Command line call of GHC:
```
~/ghc/inplace/bin/ghc-stage2 \
--make
-package ghc-7.11.20150209 \
-fplugin=MyPlugin \
Test.hs
```
Results in the following error
```
Module imports form a cycle:
module ‘MyPlugin’ (./MyPlugin.hs) imports itself
```
which does not seem reasonable to me understand.
### Minimal example (pragma)
On the other hand, if I change `Test.hs` to the following
```hs
{-# OPTIONS_GHC -fplugin MyPlugin #-}
module Test where
main :: IO ()
main = return ()
```
and calling GHC like this
```
~/ghc/inplace/bin/ghc-stage2 \
--make \
-package ghc-7.11.20150209 \
-dynamic \
Test.hs
```
it works.
I did not change `MyPlugin.hs`.
### Note
1. Using `-fplugin=MyPlugin` vs. `-fplugin MyPlugin` does not make a difference.
1. The command line example behaves the same independent of whether I supply the `-dynamic` flag or not.
1. I had to add the `-dynamic` flag, because otherwise GHC will complain that:
`
<no location info>:
cannot find normal object file ‘./MyPlugin.dyn_o’
while linking an interpreted expression
`
This might be a long shot, but maybe using the `-fplugin` option should imply the `-dynamic` flag?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| 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":"Providing type checker plugin on command line results in false cyclic import error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":["cycle","imports","plugin","typechecker"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I am playing around with the new type checker plugins using the current development branch of GHC. When I supply the plugin module to GHC through the command line I get a cyclic import error message, which I think is false. If I supply the same plugin module using a pragma I do not get an error message.\r\n\r\n=== Minimal Example (Command Line)\r\n\r\n`MyPlugin.hs`:\r\n{{{#!hs\r\nmodule MyPlugin ( plugin ) where\r\n\r\nimport Plugins ( Plugin, defaultPlugin )\r\n\r\nplugin :: Plugin\r\nplugin = defaultPlugin\r\n}}}\r\n\r\n`Test.hs`:\r\n{{{#!hs\r\nmodule Test where\r\n\r\nmain :: IO ()\r\nmain = return ()\r\n}}}\r\n\r\nCommand line call of GHC:\r\n{{{\r\n~/ghc/inplace/bin/ghc-stage2 \\\r\n --make \r\n -package ghc-7.11.20150209 \\\r\n -fplugin=MyPlugin \\\r\n Test.hs\r\n}}}\r\n\r\nResults in the following error\r\n{{{\r\nModule imports form a cycle:\r\n module ‘MyPlugin’ (./MyPlugin.hs) imports itself\r\n}}}\r\nwhich does not seem reasonable to me understand.\r\n\r\n=== Minimal example (pragma)\r\n\r\nOn the other hand, if I change `Test.hs` to the following\r\n{{{#!hs\r\n{-# OPTIONS_GHC -fplugin MyPlugin #-} \r\nmodule Test where\r\n\r\nmain :: IO ()\r\nmain = return ()\r\n}}}\r\n\r\nand calling GHC like this\r\n{{{\r\n~/ghc/inplace/bin/ghc-stage2 \\\r\n --make \\\r\n -package ghc-7.11.20150209 \\\r\n -dynamic \\\r\n Test.hs\r\n}}}\r\nit works.\r\n\r\nI did not change `MyPlugin.hs`.\r\n\r\n=== Note\r\n\r\n 1. Using `-fplugin=MyPlugin` vs. `-fplugin MyPlugin` does not make a difference.\r\n 1. The command line example behaves the same independent of whether I supply the `-dynamic` flag or not.\r\n 1. I had to add the `-dynamic` flag, because otherwise GHC will complain that:\r\n {{{\r\n <no location info>:\r\n cannot find normal object file ‘./MyPlugin.dyn_o’\r\n while linking an interpreted expression\r\n }}}\r\n This might be a long shot, but maybe using the `-fplugin` option should imply the `-dynamic` flag?\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9980TcS monad is too heavy2019-07-07T18:38:04ZSimon Peyton JonesTcS monad is too heavyThe typechecker's constraint-solving monad, `TcS`, is simply built on top of `TcM`, but it doesn't use most of `TcM`'s facilities. That was fine while `TcS` was only called from the typechecker, but now (as part of [fixingpattern-matchov...The typechecker's constraint-solving monad, `TcS`, is simply built on top of `TcM`, but it doesn't use most of `TcM`'s facilities. That was fine while `TcS` was only called from the typechecker, but now (as part of [fixingpattern-matchoverlapchecking](pattern-match-check)) we invoke it from the desugarer.
It seems quite wrong to construct a vast, and unnecessary `TcM` context just to invoke `TcS`.
Better: make `TcS` into its own monad, with its own `TcSLclEnv`, built on `IOEnv` like the others.
Main objection: the plugins mechanism exposes `unsafeTcPluginTcM`, which would become unavailable. But it it used?