GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-10-13T14:34:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/21447Confusing GADTSyntax newtype error with invisible kinds2022-10-13T14:34:21Zsheafsam.derbyshire@gmail.comConfusing GADTSyntax newtype error with invisible kindsConsider the following:
```haskell
type N :: TYPE r -> Type
newtype N a where
MkN :: (a -> N a) -> N a
```
This seems fine, right? Except that the user didn't write a forall in the type of `MkN`, so the kind of `a` is defaulted. Maki...Consider the following:
```haskell
type N :: TYPE r -> Type
newtype N a where
MkN :: (a -> N a) -> N a
```
This seems fine, right? Except that the user didn't write a forall in the type of `MkN`, so the kind of `a` is defaulted. Making the kinds explicit, it's as if we wrote:
```haskell
type N :: forall (r :: RuntimeRep). TYPE r -> Type
newtype N @r a where
MkN :: (a -> N a) -> N @LiftedRep a
```
and this isn't allowed: we can't have a newtype which is a genuine GADT, where the type variables in the return kind don't match those in the head of the declaration.
However, the error message is quite confusing:
```
* A newtype constructor must have a return type of form T a1 ... an
MkN :: forall a. (a -> N a) -> N a
* In the definition of data constructor `MkN'
In the newtype declaration for `N'
|
10 | MkN :: (a -> N a) -> N a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```9.6.1Finley McIlwaineFinley McIlwainehttps://gitlab.haskell.org/ghc/ghc/-/issues/21405Assertion in reportWanteds is too strict2023-02-01T08:38:59Zsheafsam.derbyshire@gmail.comAssertion in reportWanteds is too strictThere's an assertion in `reportWanteds` that checks that we aren't suppressing all the errors.
```haskell
-- This check makes sure that we aren't suppressing the only error that will
-- actually stop compilation
; ...There's an assertion in `reportWanteds` that checks that we aren't suppressing all the errors.
```haskell
-- This check makes sure that we aren't suppressing the only error that will
-- actually stop compilation
; massert $
null simples || -- no errors to report here
any ignoreConstraint simples || -- one error is ignorable (is reported elsewhere)
not (all ei_suppress tidy_items) -- not all errors are suppressed
```
This is in the context of "Wanteds rewrite Wanteds", where we should always have one non-rewritten Wanted to report to the user.
This makes sense, but it doesn't seem to take into account implications. For instance, we could have an implication:
```
[W] hole{co1}
===>
[W] hole{co2} {{co1}} :: alpha ~# (beta |> co)
```
When we call `reportWanteds` on this implication, we have the unsolved unrewritten `[W] hole{co1}` to report. Fine. Then we recurse into the implication, and we have a single constraint `[W] hole{co2}` to report, which has been rewritten by `[W] hole{co1}`. This trips up the assertion (we only have rewritten Wanteds to report), even though at an outer level we reported an unrewritten Wanted.
@rae, do you agree that the assertion is wrong?https://gitlab.haskell.org/ghc/ghc/-/issues/21404decideMonoTyVars doesn't handle coercion variables in "candidates"2022-04-27T17:38:37Zsheafsam.derbyshire@gmail.comdecideMonoTyVars doesn't handle coercion variables in "candidates"In `decideMonoTyVars` we find:
```haskell
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
...
co_vars = coVarsOfTypes (psig_tys ++ taus)
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
.....In `decideMonoTyVars` we find:
```haskell
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
...
co_vars = coVarsOfTypes (psig_tys ++ taus)
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
...
mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1
```
Note that `closeWrtFunDeps` expects a set of type variables closed over kinds. However, `mono_tvs1` doesn't seem to be closed over kinds, in general:
1. `tyCoVarsOfTypes` is deep, so `tyCoVarsOfTypes candidates` is closed over kinds.
2. We filter out some variables using `isQuantifiableTv`. How do we know this set is still closed over kinds? In particular, we might have kept a coercion variable but not the type variables found in its kind.
I ran into the following example while working on a patch:
Candidates:
- `{co} :: gamma[conc] ~# F`
- `alpha[tau:1] ~# (beta[tau:1] |> TYPE {co})`
At `TcLevel` 0, `mono_tvs0 = {co}`, `closeOverKinds mono_tvs0 = {co, gamma}`.
@rae, what am I missing? Is the above collection of candidates somehow ill-formed, i.e. doesn't uphold some invariant required to pass it to `decideMonoTyVars`?https://gitlab.haskell.org/ghc/ghc/-/issues/21366RULE quantification over equalities is fragile2022-04-12T21:26:53Zsheafsam.derbyshire@gmail.comRULE quantification over equalities is fragileWe quantify over some equality constraints arising from the LHS of rules, as explained in `Note [RULE quantification over equalities]`. We do so by inspecting the initial LHS Wanted constraints, before we have even attempted to canonical...We quantify over some equality constraints arising from the LHS of rules, as explained in `Note [RULE quantification over equalities]`. We do so by inspecting the initial LHS Wanted constraints, before we have even attempted to canonicalise anything. This seems a bit fragile; for example, we are willing to quantify over equalities of the form `A ~# F B` for a type family `F`, but what if the constraint was of the form `D A ~# D (F B)` for a datatype `D`? We would now decide **not** to quantify over it because neither the LHS or RHS is headed by a type family, even though it is decomposable and decomposes to `A ~# F B`, which we would quantify over.
Here's a contrived example I came up with that illustrates the problem:
```haskell
type I :: k -> k
type family I a where
I a = a
f :: forall rr (a :: TYPE (I rr)). Proxy rr -> Proxy a -> Proxy a
f _ px = px
{-# NOINLINE f #-}
{-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}
```
```
warning:
Forall'd constraint `LiftedRep ~ I LiftedRep'
is not bound in RULE lhs
Orig bndrs: [co_aBT, k, x]
Orig lhs: f @LiftedRep @Int k x
optimised lhs: f @LiftedRep @Int k x
|
16 | {-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/21346GHC no longer instantiates representation-polymorphic newtype constructors2022-06-10T10:36:35Zsheafsam.derbyshire@gmail.comGHC no longer instantiates representation-polymorphic newtype constructorsConsider the following program:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UnliftedNewtypes #-}
import GHC.Exts
newtype N r (a :: TYPE r) = MkN a
foo :: Int# -> N IntRep I...Consider the following program:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UnliftedNewtypes #-}
import GHC.Exts
newtype N r (a :: TYPE r) = MkN a
foo :: Int# -> N IntRep Int#
foo i = MkN i
```
On GHC 9.2, the output of `-ddump-ds-preopt` is:
```haskell
foo = \ (i :: Int#) -> (\ (ds :: Int#) -> MkN @'IntRep @Int# ds) i
```
That is, we have instantiated the representation-polymorphic `MkN :: forall r (a :: TYPE r) . a -> N r a`, with `MkN @IntRep @Int#`.
However, on GHC HEAD, we get:
```haskell
foo = \ (i :: Int#) -> (\ @(r :: RuntimeRep) @(a :: TYPE r) (ds :: a) -> MkN @r @a ds) i
```
here we have a representation-polymorphic binder `ds :: a`!
I think this issue was introduced in !5640. There used to be logic in `tc_infer_id` to instantiate a representation-polymorphic data constructor, but that logic seems to have vanished entirely, and the new `tcInferDataCon` function does not do any instantiation. It's left with the original argument types, and thus `dsConLike` gets passed argument types which don't have a fixed runtime representation.
I think we should have an invariant that the argument types stored in `ConLikeTc` have a syntactically fixed RuntimeRep, which is necessary as they are the types of variables bound in a lambda (created by `dsConLike`), and enforce it by instantiating the newtype constructor.
This issue is causing me trouble with the implementation of PHASE 2 of FixedRuntimeRep.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21330Add origins to meta-variables2023-08-28T11:06:27Zsheafsam.derbyshire@gmail.comAdd origins to meta-variablesSimon suggests that we should add origins for metavariables (e.g. "alpha arose from the instantiation of the function `f`"). This could either be a field of the `MetaTv` constructor of `TcTyVarDetails`, or we could have different origins...Simon suggests that we should add origins for metavariables (e.g. "alpha arose from the instantiation of the function `f`"). This could either be a field of the `MetaTv` constructor of `TcTyVarDetails`, or we could have different origins for different kinds of type variables. When unifying metavariables, we will need to combine the origins. Simon suggests that, to start off, we can simply pick the most informative origin and discard the other.
In !7812 I added origins for `ConcreteTv` type variables, but extending this to other kinds of metavariables could improve error messages.https://gitlab.haskell.org/ghc/ghc/-/issues/21309Order dependence in type checking with the monomorphism restriction2022-04-25T01:39:53ZRichard Eisenbergrae@richarde.devOrder dependence in type checking with the monomorphism restrictionThe order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes...The order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes, though, a constraint can be eagerly solved, making it disappear (and thus not affecting any variables).
A nested example:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
class C a b where
method :: a -> b -> ()
instance C Char b where
method _ _ = ()
f1 x = let g = \y -> method x y in
(x : "hi", (g True, g Nothing))
f2 x = (x : "hi",
let g = \y -> method x y in
(g True, g Nothing))
```
`f1` is rejected, as `method x y` gives rise to `[W] C alpha beta`, which cannot be solved. Then, `g` is not generalised, so we get `g :: beta -> ()`, which is not general enough for its two usages.
`f2` is accepted, as `method x y` gives rise to `[W] C Char beta`, easily solved by the instance. No MR happens.
A top-level example:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug2 where
x = 5
class C a b where
method :: a -> b -> ()
instance C Int b where
method _ _ = ()
x2 :: (Int, ((), ()))
x2 = (x + 1, (g True, g 'x')) -- remove references to 'g' to allow module to be accepted
g = \y -> method x y
x3 :: ((), ())
x3 = (g True, g 'x')
```
This is rejected. Note that `x2` depends on `g`, and thus `g` is type-checked first -- critically, before we know that `x :: Int`. So the MR kicks in and prevents generalisation. However if we change to `x2 = (x + 1, ((), ()))`, then the module is accepted: `x2` gets seen first, we learn that `x :: Int`, and then there is no constraint to prevent generalisation in `g`. The two different uses in `x3` are accepted.
I don't think this will be easy to fix: we would somehow need to delay the computation of whether or not to generalise, and that seems Very Hard. Maybe this just gets filed in the user manual under `FlexibleInstances` and how flexibility can sometimes cause trouble? Not sure. Note that "let should not be generalised" is not enough here, because the problem can manifest at top-level.
This is based on a conversation with @simonpj this morning; credit to him for outlining the problem.https://gitlab.haskell.org/ghc/ghc/-/issues/21289Type-changing record update ignores type families2022-05-26T07:42:42ZRichard Eisenbergrae@richarde.devType-changing record update ignores type familiesI would like this to compile:
```hs
type family F (a :: Bool)
type instance F True = Int
type instance F False = Int
type family G (a :: Bool)
type instance G True = Int
type instance G False = Bool
data Rec a = MkR { konst :: F a
...I would like this to compile:
```hs
type family F (a :: Bool)
type instance F True = Int
type instance F False = Int
type family G (a :: Bool)
type instance G True = Int
type instance G False = Bool
data Rec a = MkR { konst :: F a
, change :: G a }
ch :: Rec True -> Rec False
ch r = r { change = False }
```
The `ch` function does a type-changing record update. Normally, a type-changing record update can be written only when all fields that mention the changing type variable are updated. And `ch` does not update `konst`, whose type mentions `a`. But it's OK, actually: because `F True` (old type) and `F False` (new type) are actually both `Int`, all is well. Yet GHC rejects.
Unlike some bugs I report, this one is from a Real Use Case. (I have a practical, fancy-typed library I'm building that wants to ensure that a particular record-update updates certain fields.)
While in town, should probably also fix #10856 and transitively #2595 (which, I think, is effectively a dup of #10856).https://gitlab.haskell.org/ghc/ghc/-/issues/21239Add syntactic equality relation2022-04-28T23:29:28Zsheafsam.derbyshire@gmail.comAdd syntactic equality relationIn several places, it would be useful to have a syntactic equality relation, `~S#`.
* Under this relation, two types are equal if they respond equal to `tcEqType`, up to zonking.
(This means: no rewriting, but we can zonk and look thr...In several places, it would be useful to have a syntactic equality relation, `~S#`.
* Under this relation, two types are equal if they respond equal to `tcEqType`, up to zonking.
(This means: no rewriting, but we can zonk and look through type synonyms.)
* The evidence for `t1 ~S# t2` is always Refl.
With such an equality relation, we could:
* **Get rid of `IsRefl#`**. Currently, the representation polymorphism checks emit a nominal equality `ki ~# concrete_tv`, and when we don't support rewriting (because of [PHASE 1 of `FixedRuntimeRep`](https://gitlab.haskell.org/ghc/ghc/-/wikis/FixedRuntimeRep)) we additionally emit `IsRefl# ki concrete_tv`. Instead, we should syntactically unify `ki` with `concrete_tv` in PHASE 1.
* **Enforce a specific runtime rep**. Suppose we want to enforce that a type `ty :: TYPE rr` has a specific runtime representation `specific_rr`, without any coercions needed, (e.g. `LiftedRep` if we want to enforce liftedness). Then we can syntactically unify `rr` with `specific_rr`. Example of when this is useful: `\x -> (x, True)`. At the lambda, `x` comes into scope with type `x :: alpha :: TYPE rr`. Later we find that it must be lifted because it's an argument to the tuple.
## Implementation
A useful property of `(~S#)` is that it can be solved or refuted without ever generating any constraints. So this should **NOT** be a new constructor of `EqRel`, because we have no need for a syntactic equality predicate. All we need is a counterpart to `uType` that works at the syntactic level, doing unification as it goes, and *never deferring to the main constraint solver*.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21210Quantified constraint should be accepted in RHS of type family equation2022-03-15T15:33:45ZRichard Eisenbergrae@richarde.devQuantified constraint should be accepted in RHS of type family equationThis is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Ch...This is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Char -> p Double -> Bool
f1 p1 p2 = p1 == p1 && p2 == p2
type ForallEq p = forall x. Eq (p x)
f2 :: ForallEq p => p Char -> p Double -> Bool
f2 p1 p2 = p1 == p1 && p2 == p2
type ForallEqs :: [Type -> Type] -> Constraint
type family ForallEqs ps where
ForallEqs '[] = ()
ForallEqs (p : ps) = (ForallEq p, ForallEqs ps)
```
The `forall` in a quantified constraint is really a different `forall` than the one used in normal types, and it should be acceptable in the RHS of a type family equation.https://gitlab.haskell.org/ghc/ghc/-/issues/21206lookupIdSubst panic with indexed monad2024-02-05T22:55:26ZTobias HasloplookupIdSubst panic with indexed monadSee also
* #22788
* #23147
## Summary
Compiling causes a panic. I initially observed this with GHC 9.2.1
I noticed that the panic looks similar to the panic from #20820, for which there is the fix !7664. Since !7664 has not been mer...See also
* #22788
* #23147
## Summary
Compiling causes a panic. I initially observed this with GHC 9.2.1
I noticed that the panic looks similar to the panic from #20820, for which there is the fix !7664. Since !7664 has not been merged yet, I tried compiling the code with a [CI-build that contains the fix](https://gitlab.haskell.org/ghc/ghc/-/jobs/959784). That CI-build panics too.
## Steps to reproduce
Compile this cabal project with a recent GHC:
[lookupidsubst-panic.zip](/uploads/edbf21a3bd8d0ba7e0a252863532d90d/lookupidsubst-panic.zip)
```
PS C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic> cabal build --with-compiler="C:\Program Files\ghc-9.3.20220225-x86_64-unknown-mingw32\bin\ghc-9.3.20220225.exe"
Resolving dependencies...
Build profile: -w ghc-9.3.20220225 -O1
In order, the following will be built (use -v for more details):
- lookupidsubst-panic-0.1.0.0 (exe:lookupidsubst-panic) (first run)
Configuring executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
Preprocessing executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
Building executable 'lookupidsubst-panic' for lookupidsubst-panic-0.1.0.0..
<no location info>: warning: [-Wmissing-home-modules]
These modules are needed for compilation but not listed in your .cabal file's other-modules:
Base Demonad TypeState
[1 of 5] Compiling Base ( app\Base.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Base.o )
[2 of 5] Compiling Demonad ( app\Demonad.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Demonad.o )
[3 of 5] Compiling TypeState ( app\TypeState.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\TypeState.o )
[4 of 5] Compiling Main ( app\Main.hs, C:\Users\Tobias\Documents\Uni\haskell\lookupidsubst-panic\dist-newstyle\build\x86_64-windows\ghc-9.3.20220225\lookupidsubst-panic-0.1.0.0\x\lookupidsubst-panic\build\lookupidsubst-panic\lookupidsubst-panic-tmp\Main.o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20220225:
lookupIdSubst
$dNum_a26l
InScope {i_a25Y $dDemonad_a269 $creturnIx_a2gd $cbindIx_a2gY
$cseqIx'_a2ir $krep_a2kH $krep_a2kI $krep_a2kJ $krep_a2kK
$krep_a2kL $krep_a2kM $krep_a2kN $krep_a2kO $krep_a2kP $krep_a2kQ
$krep_a2kR $krep_a2kS $krep_a2kT $krep_a2kU $krep_a2kV $krep_a2kW
$krep_a2kX $krep_a2kY $krep_a2kZ $krep_a2l0 $krep_a2l1 $krep_a2l2
$krep_a2l3 $krep_a2l4 $krep_a2l5 $krep_a2l6 $krep_a2l7 $krep_a2l8
$krep_a2l9 $krep_a2la $krep_a2lb $krep_a2lc $krep_a2ld $krep_a2le
$krep_a2lf runSt add1 solve1 val1 $tc'Satisfied $tc'Unsatisfied
$tc'Interrupted $tcTerminatedSolverRun $tc'MkStRes $tcStRes
$tc'MkSt $tcSt $fDemonadkSt $tc'MkVarVal $tcVarVal $trModule}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\\GHC\\Utils\\Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Core\Subst.hs:260:17 in ghc:GHC.Core.Subst
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Expected behavior
I expect the code to compile successfully. Alternatively I expect a sensible error message but not a panic.
## Environment
* GHC version used: https://gitlab.haskell.org/ghc/ghc/-/jobs/959784
* Operating System: Windowshttps://gitlab.haskell.org/ghc/ghc/-/issues/21199(GHC 9.2.2) Impossible happened...2022-07-28T10:15:10ZAdam Conner-Sax(GHC 9.2.2) Impossible happened...## Summary
GHC 9.2.2 compiler reports "The impossible happened"
```
ghc-9.2.2: panic! (the 'impossible' happened)
(GHC version 9.2.2:
mightEqualLater finds an unbound cbv
cbv_a1TC[cbv:1]
[]
Call stack:
CallStack (from Has...## Summary
GHC 9.2.2 compiler reports "The impossible happened"
```
ghc-9.2.2: panic! (the 'impossible' happened)
(GHC version 9.2.2:
mightEqualLater finds an unbound cbv
cbv_a1TC[cbv:1]
[]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Solver/Monad.hs:2587:16 in ghc:GHC.Tc.Solver.Monad
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Build the repo (https://github.com/adamConnerSax/impossible922) with ghc 9.2.2
## Expected behavior
I expect it to build (as it does with ghc 8.10.7)
## Environment
GHC 9.2.2 (optionally ghc 8.10.7), cabal 3.6.2 (all installed with ghcup)
Optional:
* Operating system: MacOs 12.2.1
* System Architecture: Mac Pro (tower, late 2013)9.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/21139Unfoldings in interface files are sucked in too eagerly2022-02-26T12:48:59ZSimon Peyton JonesUnfoldings in interface files are sucked in too eagerlyThis ticket is a standalone report of a discovery we made in a merge request discussion !6735; specifically [this comment](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6735#note_389262).
There is a long-standing bug in typecking...This ticket is a standalone report of a discovery we made in a merge request discussion !6735; specifically [this comment](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6735#note_389262).
There is a long-standing bug in typecking the unfoldings from interface files.
* A call to `hasNoBinding` will force the Id's `Unfolding`
* Because of a bug in `tcUnfolding` (see below), that will force the thunk created by `tcPragExpr`
* And that lint the rhs before returning it
* And Linting will call `hasNoBinding` on Ids mentioned in the rhs
* Which will force their unfoldings
* And so on.
Never mind loops -- this forces way too much stuff to get sucked in from interface files -- essentially the transitive closure of everything.
Other notes:
* **TODO** `tcPragExpr` should be renamed to be `tcUnfoldingRhs`.
* `Note [Linting Unfoldings from Interfaces]` is nothing to do with loops. Consider this decl in an interface file M.hi:
```
f = \x. let y = blah in blah2
```
When we Lint f's unfolding we will Lint y's unfolding too: see
```
lintLetBind top_lvl rec_flag binder rhs rhs_ty
= do { ...
; ; addLoc (UnfoldingOf binder) $
lintIdUnfolding binder binder_ty (idUnfolding binder)
```
So there is no point in *also* Linting y's unfolding during `tcIfaceExpr` on f's RHS. That's all. **TODO** Could the Note be make clearer?
* I don't see how `idUnfolding` vs `realIdUnfolding` makes the slightest difference. The difference is only that the former consults OccInfo first.
The Real Bug is here:
```
tcUnfolding toplvl name _ info (IfCoreUnfold stable if_expr)
= do { uf_opts <- unfoldingOpts <$> getDynFlags
; mb_expr <- tcPragExpr False toplvl name if_expr
; ...
; return $ case mb_expr of
Nothing -> NoUnfolding
Just expr -> mkFinalUnfolding uf_opts unf_src strict_sig expr
}
```
Notice that to choose between `NoUnfolding` and `CoreUnfolding` (which is returned by `mkFinalUnfolding`), we force `mb_expr`. **ALAS**! That is the very thunk we are trying delay forcing!
I think we should always return a `CoreUnfolding` thus:
```
; return $ mkFinalUnfolding uf_opts unf_src strict_sig
(case mb_expr of { Just e -> e; Nothing -> panic })
```
Or, more directly, use `forkM` (not `forkM_maybe`) in `tcPragExpr`.
This is just what Sam suggests:
> What I am trying to do currently is to architect `tcUnfolding` so that it immediately returns an unfolding which we can inspect to obtain the value of `hasNoBinding`
Why do we *ever* use `forkM_maybe`? There is a mysterious comment:
```
forkM_maybe doc thing_inside
= do { unsafeInterleaveM $
do { traceIf (text "Starting fork {" <+> doc)
; mb_res <- tryM thing_inside ;
case mb_res of
Right r -> do { traceIf (text "} ending fork" <+> doc)
; return (Just r) }
Left exn -> do {
-- Bleat about errors in the forked thread, if -ddump-if-trace is on
-- Otherwise we silently discard errors. Errors can legitimately
-- happen when compiling interface signatures (see tcInterfaceSigs)
ifOptM Opt_D_dump_if_trace
(print_errs (hang (text "forkM failed:" <+> doc)
4 (text (show exn))))
```
I have no idea what these "legitimate" errors are. git-blame tells me that this
comment dates back to before this 2003 commit:
```
commit 98688c6e8fd33f31c51218cf93cbf03fe3a5e73d
Author: simonpj <unknown>
Date: Thu Oct 9 11:59:43 2003 +0000
[project @ 2003-10-09 11:58:39 by simonpj]
-------------------------
GHC heart/lung transplant
-------------------------
This major commit changes the way that GHC deals with importing
types and functions defined in other modules, during renaming and
typechecking. On the way I've changed or cleaned up numerous other
things, including many that I probably fail to mention here.
```
Moreover this commit *removes* `tcInterfaceSigs`. So I think it's historical.
**Proposal (TODO)**: get rid of `forkM_maybe`, and use `forkM` all the time.
I think that will solve our problem. But let's leave some careful Notes to explain
this. Notably, it's important that `mkFinalUnfolding` and friends all return
a `CoreUnfolding` *without forcing the unfolding rhs*.
All clear?https://gitlab.haskell.org/ghc/ghc/-/issues/21126Definition of heterogeneous equality rejected unless using a SAKS2022-04-07T16:01:28Zsheafsam.derbyshire@gmail.comDefinition of heterogeneous equality rejected unless using a SAKSThe following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the da...The following definitions of heterogeneous equality are rejected on HEAD:
```haskell
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (a :: k1) :~~: (b :: k2) where
| ^^^^^^^^^^^^^^^^^^^^^^
```
```haskell
data (:~~:) :: k1 -> k2 -> Type where
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
Note that this remains true even if one enables `-XCUSKs`, so this doesn't fit the diagnostic of https://gitlab.haskell.org/ghc/ghc/-/issues/20752#note_394357.
The only way to get this accepted is to write a standalone kind signature:
```haskell
type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
HRefl :: a :~~: a
```
It seems to me that the "different names for the same type variable" check is overly-eager for GADTs. In particular, the following is also rejected:
```haskell
data (:~~:) :: k1 -> k2 -> Type where
NotHRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: b
HRefl :: a :~~: a
```
```
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
```
I don't know how GHC concludes that `k1` and `k2` must refer to the same kind variable there.9.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21098Report an error when applying a type family associated with a class to a type...2023-12-17T22:07:48ZMarioReport an error when applying a type family associated with a class to a type that's not an instance of the class## Summary
I wasted at least an hour on this issue, which I originally reported at https://github.com/well-typed/generics-sop/issues/152 . I'm reporting it here as suggested because I can't be the only GHC user dumb enough to be confuse...## Summary
I wasted at least an hour on this issue, which I originally reported at https://github.com/well-typed/generics-sop/issues/152 . I'm reporting it here as suggested because I can't be the only GHC user dumb enough to be confused by the behaviour.
Trying to apply a *class method* to a value whose type is an instance of the type class results in an understandable error message
> No instance for YourType arising from a use of theMethod
Trying to apply an *associated type family* to a type that's not an instance of the type class, in contrast, does not result in any error message by itself: the application will simply remain stuck.
## Steps to reproduce
```
GHCi, version 8.10.7: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /tmp/haskell-stack-ghci/2a3bbd58/ghci-script
Prelude> :module + Generics.SOP Generics.SOP.GGP
Prelude Generics.SOP Generics.SOP.GGP> :set -XDeriveGeneric
Prelude Generics.SOP Generics.SOP.GGP> newtype N = N Int deriving GHC.Generics.Generic
Prelude Generics.SOP Generics.SOP.GGP> :k! Code N
Code N :: [[*]]
= Code N
Prelude Generics.SOP Generics.SOP.GGP> :k! GCode N
GCode N :: [[*]]
= '[ '[Int]]
```
## Expected behavior
A clear error message like
> No instance for (Generic N) arising from a use of ‘Code’
## Environment
* GHC version used: 8.10.7 and 9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/21041Check laziness of Coercion in the Reduction type2023-12-04T15:08:50ZRichard Eisenbergrae@richarde.devCheck laziness of Coercion in the Reduction typeThe `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a ...The `Coercion` stored in a `Reduction` is lazy in order to work with Derived constraints. However, once !5899 lands, Derived constraints will be a part of history. We should then check to see if making this coercion strict would yield a performance improvement.https://gitlab.haskell.org/ghc/ghc/-/issues/21024A deferred type error inferferes with the monomorphism restriction2022-06-09T14:31:57ZRichard Eisenbergrae@richarde.devA deferred type error inferferes with the monomorphism restrictionHere is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GH...Here is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GHC embarrassingly infers the type `Any` for `x`, affected by the presence of the ill-typed `other`.https://gitlab.haskell.org/ghc/ghc/-/issues/21023MonoLocalBinds sometimes monomorphises *global* binds2022-03-07T22:09:56ZRichard Eisenbergrae@richarde.devMonoLocalBinds sometimes monomorphises *global* bindsHere is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`...Here is a fairly simple program:
```hs
{-# LANGUAGE MonoLocalBinds #-}
module Bug where
x = 5
f y = (x, y)
```
Important: the monomorphism restriction is in effect.
GHC embarrassingly infers the type `Any -> (Integer, Any)` for `f`. This is because `f`'s right-hand side mentions `x`, whose type is not yet known. (The monomorphism restriction means it's type is not `Num a => a`.) So, GHC chooses the `NoGen` plan for generalization. With nothing to say what the type of `y` should be, GHC picks `Any`. Bad GHC, bad. Giving `x` a type signature or disabling the monomorphism restriction fixes the problem.
I think the solution is simply never to do `NoGen` for top-level bindings.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/21006Unhelpful Kind equality error at the start of file2022-01-28T10:50:09ZJkensikUnhelpful Kind equality error at the start of fileI get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the ...I get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the constraint (Set b, Set s) are being matched? I would expect the constraint to existentially quantify the type b but why would it be matching them?
I believe the last thing I changed before getting the error was adding OpOutcome to the class.
here is the code
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import GHC.TypeLits (Symbol)
import GHC.Exts (Constraint)
import Data.Reflection (Reifies, reflect)
import Data.Proxy (Proxy(..))
main :: IO ()
main = print 5
class ((a,b)::Constraint) => HasCtxt a b
instance (a,b) => HasCtxt a b
class Determines a b | a -> b
instance Determines a b => Determines a b
type Set b = (b ~ b)
type OpLayout a = (forall s ctxt b. (OpCtxt a s b ~ ctxt, Determines a b, Determines a ctxt,Reifies s b) => ( HasCtxt ctxt (Reifies s b))) :: Constraint
data Stack a where
Cons :: OpConstructor a -> Stack b -> Stack a
Nil :: Stack "NIL"
class OpLayout a => OpCode (a::Symbol) where
type OpCtxt a s b = (ctxt :: Constraint) | ctxt -> s b
type OpOutcome a :: *
data OpConstructor a
opValue :: Determines a s => Proxy s
opValue = Proxy
popOP :: OpCtxt a s b => Stack a -> (b :: *)
evalOP :: OpConstructor a -> Stack x -> OpOutcome a
instance OpCode "load_val" where
type OpCtxt "load_val" s b = (Set s, Set b)
type OpOutcome "load_val" = Stack "load_val"
data OpConstructor "load_val" = forall b. LOAD_VAL b
popOP stack = reflect opValue
evalOP op stack = op `Cons` stack
```https://gitlab.haskell.org/ghc/ghc/-/issues/20974GHCi >= 9.2.1 prints type signatures containing type families in an ugly way2022-05-20T08:22:33ZAndrzej RybczakGHCi >= 9.2.1 prints type signatures containing type families in an ugly wayConsider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint wh...Consider the following:
```haskell
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
import Data.Kind
class A (m :: Type -> Type)
class B (m :: Type -> Type)
type family F cs (m :: Type -> Type) :: Constraint where
F '[] m = ()
F (c : cs) m = (c m, F cs m)
test :: F [Monad, A, B] m => m ()
test = pure ()
```
The type signature of `test` is pretty-printed in GHCi 9.0.2 and lower:
```
$ ghci-9.0.2
GHCi, version 9.0.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, A m, B m) => m ()
```
but this is what happens in 9.2.1 and HEAD:
```
$ ghci-9.2.1
GHCi, version 9.2.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/unknown/.ghci
>>> :l test.hs
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, one module loaded.
>>> :t test
test :: (Monad m, (A m, (B m, () :: Constraint))) => m ()
```
Looks much worse and I'd consider that a regression.9.2.2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.com