GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-02-05T17:53:15Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24335Several bugs with forall (cv::t1~#t2). ty)2024-02-05T17:53:15ZSimon Peyton JonesSeveral bugs with forall (cv::t1~#t2). ty)In principle, GHC supports *coercion variable* in a forall-type. Thus a type can look like `forall (cv:t1~#t2). body_ty`, where `body_ty` can mention the coercion variable `cv`.
See `Note [Why ForAllTy can quantify over a coercion varia...In principle, GHC supports *coercion variable* in a forall-type. Thus a type can look like `forall (cv:t1~#t2). body_ty`, where `body_ty` can mention the coercion variable `cv`.
See `Note [Why ForAllTy can quantify over a coercion variable]` in GHC.Core.TyCo.Rep.
But I discover that GHC has multiple bugs if you actually have any terms with such a type. Here are the four bugs I have found
* `typeKind ty` simply loops if given a type that quantifies over a coercion variable. (It's a trivial bug, easily fixed, but longstanding.)
* Core Lint (specifically `lintCoArg`) complains if it sees an application `(f co)` where `f` has type `(forall (cv:t1~#t2). blah)`. (More usually `f` has type `(t1~#t2)=>blah`, when `blah` does not mention `cv`.)
* `GHC.Core.Opt.Arity.typeArity`/typeOneShots didn't count coercion arguments
if the type was (forall cv. blah)
* `GHC.Core.Opt.Simplify.Iteration.simpl_lam` (which deals with bete-reduction) crashed
when the function type looks like `(forall cv. blah)` and the application has a coercion argument.
I discovered this when working on !11492 which fixes #3781. When compiling `base:Data/Typeable/Internal.hs` the float-out pass yielded this function:
```
lvl_sjWn
:: forall (r :: RuntimeRep) k1 (co['Many] :: k1 ~# TYPE r)
(b :: k1) (r :: RuntimeRep) k2 k1 (a :: k1 -> k2).
(a ~# (->) (b |> co), (k1 -> k2) ~# (TYPE r -> *)) =>
TypeRep ((->) (b |> co)) -> TypeRep a -> Void
[LclId, Arity=5, Str=<L><L><L><L><L>b, Cpr=b]
lvl_sjWn
= \ (@(r_a2ru :: RuntimeRep))
(@k1_a2qV)
(co_a2rv :: k1_a2qV ~# TYPE r_a2ru)
(@(b_a2qX :: k1_a2qV))
(@(r_a2rJ :: RuntimeRep))
(@k2_a2qQ)
(@k1_a2qP)
(@(a_a2qR :: k1_a2qP -> k2_a2qQ))
(co_a2gm :: a_a2qR ~# (->) (b_a2qX |> co_a2rv))
(co_a2gl :: (k1_a2qP -> k2_a2qQ) ~# (TYPE r_a2rJ -> *))
(a_sjPk :: TypeRep ((->) (b_a2qX |> co_a2rv)))
(rep_a1ka :: TypeRep a_a2qR) ->
raise#
@'Lifted
@LiftedRep
@SomeException
@Void
(noinline
@([Char] -> SomeException)
errorCallException
(augment
@Char
lvl_sjWi
(augment
@Char
(\ (@b_ajEq)
(c_ajEr [OS=OneShot] :: Char -> b_ajEq -> b_ajEq)
(n_ajEs [OS=OneShot] :: b_ajEq) ->
foldr
@Char
@b_ajEq
c_ajEr
n_ajEs
(showTypeable
@(TYPE r_a2rJ -> *)
@((->) (b_a2qX |> co_a2rv))
lvl_sjWj
a_sjPk
([] @Char)))
(augment
@Char
lvl_sjWl
(showTypeable
@(TYPE r_a2rJ -> *)
@((->) (b_a2qX |> co_a2rv))
lvl_sjWm
(rep_a1ka
`cast` ((TypeRep co_a2gl co_a2gm)_R
:: TypeRep a_a2qR ~R# TypeRep ((->) (b_a2qX |> co_a2rv))))
([] @Char))))))
```
Somehow this has never happened before!https://gitlab.haskell.org/ghc/ghc/-/issues/24333Unexpected variable untouchable inside constraint since GHC 9.82024-01-16T15:36:46ZShea Levyshea@shealevy.comUnexpected variable untouchable inside constraint since GHC 9.8## Summary
With GHC 9.2.4 and GHC 9.6.2, this compiles:
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Main where
import Data.Coerce
satisfyConstraint :: (forall x y. Coercible x y => Coercible (m x...## Summary
With GHC 9.2.4 and GHC 9.6.2, this compiles:
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Main where
import Data.Coerce
satisfyConstraint :: (forall x y. Coercible x y => Coercible (m x) (m y)) => ((forall x y. Coercible x y => Coercible (m x) (m y)) => m a) -> m a
satisfyConstraint go = go
main :: IO ()
main = do
satisfyConstraint $ pure ()
pure ()
```
However, with 9.8.1, I get:
```
Test.hs:12:28: error: [GHC-83865]
• Couldn't match expected type ‘a0’ with actual type ‘()’
‘a0’ is untouchable
inside the constraints: forall x y.
Coercible x y =>
Coercible (IO x) (IO y)
bound by a type expected by the context:
(forall x y. Coercible x y => Coercible (IO x) (IO y)) => IO a0
at Test.hs:12:23-29
• In the first argument of ‘pure’, namely ‘()’
In the second argument of ‘($)’, namely ‘pure ()’
In a stmt of a 'do' block: satisfyConstraint $ pure ()
|
12 | satisfyConstraint $ pure ()
| ^^
```
## Environment
* GHC version used: 9.2.4, 9.6.2, 9.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/24176Panic with QuantifiedConstraints + RequiredTypeArguments2023-12-04T16:47:17ZKrzysztof GogolewskiPanic with QuantifiedConstraints + RequiredTypeArgumentsThis code causes a panic in master:
```haskell
{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
module T where
f :: (forall a -> Eq a) => a
f = f
```
```
<no location info>: error:
panic! (the 'impossible' happened)
...This code causes a panic in master:
```haskell
{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
module T where
f :: (forall a -> Eq a) => a
f = f
```
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.9.20231110:
instDFunTypes
df_aIu
[Just a_aIB[sk:2]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:186:37 in ghc-9.9-inplace:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Utils/Instantiate.hs:371:16 in ghc-9.9-inplace:GHC.Tc.Utils.Instantiate
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:511:29 in ghc-9.9-inplace:GHC.Utils.Error
```
I think we should enforce that `forall a -> ...` is always used with `TYPE rep`. For `forall a. ...`, the body can also be a constraint; the situation is more complicated and covered by #22063. Finally, we accept `forall {a}. Eq a` which seems to give the same result as `forall a. Eq a`, presumably we should reject it.Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/24064GHC panic with a code with type equality constraints with doubly applied type...2023-10-20T19:29:20ZIan-Woo KimGHC panic with a code with type equality constraints with doubly applied type family## Summary
With the following code which should not pass type checking, GHC panic at PostTc phase when doing `lookupIdSubst`.
The code has type equality of form F1 (F2 x) ~ F3 y, and I think that's where the bug is triggered, but the pa...## Summary
With the following code which should not pass type checking, GHC panic at PostTc phase when doing `lookupIdSubst`.
The code has type equality of form F1 (F2 x) ~ F3 y, and I think that's where the bug is triggered, but the panic happens only when combined with other statements in do-notation. (otherwise, usual type error happened, so this is my best minimization up to now).
## Steps to reproduce
```
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
class C1 b where
type F1 b
class C2 (m :: * -> *) where
type F2 m
class C3 r where
type F3 r
class G t m where
g :: m a -> t m a
data Y
data X e a
data H a
data S a
fun1 :: X e ()
fun1 = undefined
fun2 :: S ()
fun2 = undefined
fun3 :: H ()
fun3 = undefined
fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
fun4 = undefined
test :: (C2 m, F2 m ~ Y) => m ()
test = do
fun1
fun2
g fun3
fun4 undefined
main :: IO ()
main = pure ()
```
when running GHC, one will see the following panic error.
```
$ ghc Panic.hs
[1 of 2] Compiling Main ( Panic.hs, Panic.o )
Panic.hs:11:16: warning: [GHC-39567] [-Wstar-is-type]
Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
relies on the StarIsType extension, which will become
deprecated in the future.
Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
|
11 | class C2 (m :: * -> *) where
| ^
Panic.hs:11:21: warning: [GHC-39567] [-Wstar-is-type]
Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
relies on the StarIsType extension, which will become
deprecated in the future.
Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
|
11 | class C2 (m :: * -> *) where
| ^
Panic.hs:37:15: warning: [GHC-58520] [-Wtype-equality-requires-operators]
The use of ‘~’ without TypeOperators
will become an error in a future GHC release.
Suggested fix: Perhaps you intended to use TypeOperators
|
37 | fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
| ^
Panic.hs:40:21: warning: [GHC-58520] [-Wtype-equality-requires-operators]
The use of ‘~’ without TypeOperators
will become an error in a future GHC release.
Suggested fix: Perhaps you intended to use TypeOperators
|
40 | test :: (C2 m, F2 m ~ Y) => m ()
| ^
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.2:
lookupIdSubst
$dMonad_aWA
InScope {$dIP_aUI $dIP_aUN m_aUW $dC2_aUX $d~_aUY $krep_aWW
$krep_aWX $krep_aWY $krep_aWZ $krep_aX0 $krep_aX1 $krep_aX2
$krep_aX3 $krep_aX4 fun1 fun2 fun3 fun4 $tcC1 $tc'C:C1 $tcC2
$tc'C:C2 $tcC3 $tc'C:C3 $tcG $tcY $tcX $tcH $tcS $trModule}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Subst.hs:197:17 in ghc:GHC.Core.Subst
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
```
## Expected behavior
This should give a type error and stop there, not proceeding to PostTc phase.
## Environment
* GHC version used: ghc 9.6.2
* Operating System: macOS Ventura 13.5.2Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/23903GHC 9.6 panics when encountering representation-polymorphic type hidden behin...2023-08-29T20:55:03ZAlex IonescuGHC 9.6 panics when encountering representation-polymorphic type hidden behind type family## Summary
GHC 9.6 panics when encountering an illegal representation-polymorphic type that is hidden behind a type family, instead of reporting the appropriate error (GHC-55287). The issue occurs with both GHC 9.6.2 and 9.6.1, but does...## Summary
GHC 9.6 panics when encountering an illegal representation-polymorphic type that is hidden behind a type family, instead of reporting the appropriate error (GHC-55287). The issue occurs with both GHC 9.6.2 and 9.6.1, but doesn't occur with GHC 9.4.7 and 9.2.8.
## Steps to reproduce
Below is the offending code:
```haskell
{-# LANGUAGE GHC2021, AllowAmbiguousTypes, DataKinds, MagicHash, TypeFamilies #-}
module Unboxed where
import Data.Kind(Type)
import GHC.Exts(Float#, Int#, RuntimeRep(FloatRep, IntRep), TYPE)
type Rep :: Type -> RuntimeRep
type family Rep t where
Rep Int = IntRep
Rep Float = FloatRep
type Unbox :: forall (t :: Type) -> TYPE (Rep t)
type family Unbox t where
Unbox Int = Int#
Unbox Float = Float#
type family a #-> b where
a #-> b = Unbox a -> b
f :: a #-> ()
f _ = ()
```
Attempting to compile the above module results in a Core Lint error and a panic:
```sh
> ghc-9.6.2 -dcore-lint Unboxed.hs
[1 of 1] Compiling Unboxed ( Unboxed.hs, Unboxed.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
Unboxed.hs:20:1: warning:
Binder does not have a fixed runtime representation: ds_dIa :: (Unbox
a_aHC :: TYPE (Rep a_aHC))
In the RHS of f :: forall a. a #-> ()
In the body of lambda with binder a_aHC :: *
In the body of lambda with binder ds_dIa :: Unbox a_aHC
Substitution: <InScope = {a_aHC}
IdSubst = []
TvSubst = [aHC :-> a_aHC]
CvSubst = []>
*** Offending Program ***
f :: forall a. a #-> ()
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True,
Value=True,
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.2:
runtimeRepPrimRep
typePrimRep (Unbox a_aHC :: TYPE (Rep a_aHC))
Rep a_aHC
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Types/RepType.hs:615:5 in ghc:GHC.Types.RepType
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
If `f`'s type signature is changed to `f :: Unbox a -> ()` (i.e. inlining the body of the type family), then GHC produces the expected error message:
```sh
> ghc-9.6.2 -dcore-lint Unboxed.hs
[1 of 1] Compiling Unboxed ( Unboxed.hs, Unboxed.o )
Unboxed.hs:21:1: error: [GHC-55287]
The first pattern in the equation for ‘f’
does not have a fixed runtime representation.
Its type is:
Unbox a :: TYPE (Rep a)
|
21 | f _ = ()
| ^^^^^^^^
```
GHC 9.4.7 and 9.2.8 correctly report an error even with the type family in the signature:
```sh
> ghc-9.4.7 -dcore-lint Unboxed.hs
[1 of 1] Compiling Unboxed ( Unboxed.hs, Unboxed.o )
Unboxed.hs:21:1: error:
• The first pattern in the equation for ‘f’
does not have a fixed runtime representation.
Its type is:
p0 :: TYPE c0
Cannot unify ‘Rep a’ with the type variable ‘c0’
because it is not a concrete ‘RuntimeRep’.
• The equation for ‘f’ has one value argument,
but its type ‘a #-> ()’ has none
• Relevant bindings include
f :: a #-> () (bound at Unboxed.hs:21:1)
|
21 | f _ = ()
| ^^^^^^^^
```
```sh
> ghc-9.2.8 -dcore-lint Unboxed.hs
[1 of 1] Compiling Unboxed ( Unboxed.hs, Unboxed.o )
Unboxed.hs:21:3: error:
A levity-polymorphic type is not allowed here:
Type: Unbox a
Kind: TYPE (Rep a)
In a wildcard pattern
|
21 | f _ = ()
| ^
```
## Similar issues
While researching this, I've found 2 other similar issues involving panics and representation-polymorphic types:
* #21650
* #21544https://gitlab.haskell.org/ghc/ghc/-/issues/23884Unexpected representation-polymorphism error when using default signatures2024-01-11T21:24:47Zsheafsam.derbyshire@gmail.comUnexpected representation-polymorphism error when using default signaturesI would expect the following program from @adamgundry to work, but it doesn't:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
module T23884 where
import Data....I would expect the following program from @adamgundry to work, but it doesn't:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
module T23884 where
import Data.Kind
import GHC.Exts
type SetField :: forall {k} {r_rep} {a_rep} . k -> TYPE r_rep -> TYPE a_rep -> Constraint
class SetField x r a | x r -> a where
modifyField :: (a -> a) -> r -> r
setField :: a -> r -> r
default setField :: (a_rep ~ LiftedRep) => a -> r -> r
setField x = modifyField (\ _ -> x)
```
```
T23884.hs:16:3: error: [GHC-55287]
The first pattern in the equation for `setField'
does not have a fixed runtime representation.
Its type is:
a :: TYPE a_rep
|
16 | setField x = modifyField (\ _ -> x)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
T23884.hs:16:36: error: [GHC-55287]
* The binder of the lambda expression
does not have a fixed runtime representation.
Its type is:
a0 :: TYPE a_rep0
Cannot unify `a_rep' with the type variable `a_rep0'
because the former is not a concrete `RuntimeRep'.
* In the expression: x
In the first argument of `modifyField', namely `(\ _ -> x)'
In the expression: modifyField (\ _ -> x)
```https://gitlab.haskell.org/ghc/ghc/-/issues/23863Assertion failure for functor-combinators-0.4.1.2 with GHC 9.42023-08-23T10:31:39ZZubinAssertion failure for functor-combinators-0.4.1.2 with GHC 9.4Building `functor-combinators-0.4.1.2` with an assertion enabled GHC 9.4 results in:
```
[23 of 29] Compiling Data.HBifunctor.Tensor ( src/Data/HBifunctor/Tensor.hs, dist/build/Data/HBifunctor/Tensor.o, dist/build/Data/HBifunctor/Tenso...Building `functor-combinators-0.4.1.2` with an assertion enabled GHC 9.4 results in:
```
[23 of 29] Compiling Data.HBifunctor.Tensor ( src/Data/HBifunctor/Tensor.hs, dist/build/Data/HBifunctor/Tensor.o, dist/build/Data/HBifunctor/Tensor.dyn_o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.7:
ASSERT failed!
CanEqCanLHSFinish: (TyEq:N) not satisfied
rhs: Not
Call stack:
CallStack (from HasCallStack):
assertPprM, called at compiler/GHC/Tc/Solver/Canonical.hs:2346:10 in ghc:GHC.Tc.Solver.Canonical
```https://gitlab.haskell.org/ghc/ghc/-/issues/23827False orphan instance warning for multi-parameter type class instance2023-08-15T15:57:48ZDaneel S. YaitskovFalse orphan instance warning for multi-parameter type class instance## Summary
GHC generates orphan instance warning for a multi-param class instance, which is
located in the same module with one of type parameters, meanwhile another type parameter is
defined in another module. IMHO orphan instance war...## Summary
GHC generates orphan instance warning for a multi-param class instance, which is
located in the same module with one of type parameters, meanwhile another type parameter is
defined in another module. IMHO orphan instance warning is false positive.
## Steps to reproduce
```haskell
-- A.hs
module A where
data TofA
-- C.hs
{-# LANGUAGE FunctionalDependencies #-}
module C where
class Cof2 a b | a -> b where
-- B.hs
module B where
import A
import C
data TofB
instance Cof2 TofA TofB where
```
```
Orphan instance: instance Cof2 TofA TofB
To avoid this
move the instance declaration to the module of the class or of the type, or
wrap the type with a newtype and declare the instance on the new type.
```
## Expected behavior
Absence of orphan instance warning
## Environment
* GHC version used: 9.2.5
Optional:
* Operating System: nix-shell on top of Debian
* https://github.com/NixOS/nixpkgs/archive/aa478e283bb5c73b2cdd2f891251f0d669517b63.tar.gz
* System Architecture: intel 64bitsheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23821Defaulting plugin's proposed solution can interfere with built-in defauilting...2023-09-19T06:12:22ZGergő ÉrdiDefaulting plugin's proposed solution can interfere with built-in defauilting mechanism by writing into the same metavarsThe following defaulting plugin trys to default everything to `Int`:
```haskell
module GHC.Defaulting.INTerference (plugin) where
import GHC.Driver.Plugins
import GHC.Tc.Plugin
import GHC.Tc.Types
import GHC.Types.Var
import GHC.Tc.Uti...The following defaulting plugin trys to default everything to `Int`:
```haskell
module GHC.Defaulting.INTerference (plugin) where
import GHC.Driver.Plugins
import GHC.Tc.Plugin
import GHC.Tc.Types
import GHC.Types.Var
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Solver
import GHC.Core.Type
import GHC.Core.Class
import GHC.Data.Bag
import GHC.Builtin.Types (intTy)
plugin :: Plugin
plugin = defaultPlugin
{ defaultingPlugin = \_ -> Just DefaultingPlugin
{ dePluginInit = pure ()
, dePluginRun = \ _ -> fill
, dePluginStop = \ _ -> pure ()
}
}
fill :: WantedConstraints -> TcPluginM [DefaultingProposal]
fill wanteds = pure
[ DefaultingProposal tv [intTy] [ct]
| ct <- bagToList $ approximateWC True wanteds
, Just (cls, tys) <- pure $ getClassPredTys_maybe (ctPred ct)
, [ty] <- pure $ filterOutInvisibleTypes (classTyCon cls) tys
, Just tv <- pure $ getTyVar_maybe ty
, isMetaTyVar tv
]
```
We can try it out with a small example program:
```haskell
{-# OPTIONS_GHC -fplugin GHC.Defaulting.INTerference #-}
{-# LANGUAGE ExtendedDefaultRules #-}
class IsColor a where
op :: a -> ()
instance IsColor (Int, Int, Int) where
op _ = ()
main :: IO ()
main = pure $ op (1, 2, 3)
```
What happens here is that the plugin is called on `Num a, Num b, Num c => (a, b, c)` (the so-far inferred type of `(1, 2, 3)`) and it proposes `a ~ Int, b ~ Int, c ~ Int` (with the appropriate `Num` constraints). Since the `Num` constraints are trivally fulfillable, GHC then accepts these proposals, and thus writes `a := Int, b := Int, c := Int`. However, it then still tries to run the built-in defaulting mechanism, which proposes `a ~ Integer`, resulting in the double-write `a := Integer`.
We can see this by building a `-DDEBUG` version of GHC (e.g. `--flavour=devel2`) and looking at the relevant parts of the `-ddump-tc-trace` output:
```
defaultingPlugins {
WC {wc_simple =
[W] $dIsColor_aGj {0}:: IsColor
(a_aGl[tau:0], b_aGm[tau:0], c_aGn[tau:0]) (CDictCan)
[W] $dNum_aJL {0}:: Num a_aGl[tau:0] (CDictCan)
[W] $dNum_aJO {0}:: Num b_aGm[tau:0] (CDictCan)
[W] $dNum_aJR {0}:: Num c_aGn[tau:0] (CDictCan)}
...
writeMetaTyVar a_aGl[tau:0] := Int
...
writeMetaTyVar b_aGm[tau:0] := Int
...
writeMetaTyVar c_aGn[tau:0] := Int
...
defaultingPlugin
[DefaultingProposal a_aGl[tau:0] [Int] [[W] $dNum_aJL {0}:: Num
a_aGl[tau:0] (CDictCan)],
DefaultingProposal b_aGm[tau:0] [Int] [[W] $dNum_aJO {0}:: Num
b_aGm[tau:0] (CDictCan)],
DefaultingProposal c_aGn[tau:0] [Int] [[W] $dNum_aJR {0}:: Num
c_aGn[tau:0] (CDictCan)]]
defaultingPlugins } [True]
applyDefaultingRules {
wanteds = WC {wc_simple =
[W] $dIsColor_aGj {0}:: IsColor
(a_aGl[tau:0], b_aGm[tau:0], c_aGn[tau:0]) (CDictCan)
[W] $dNum_aJL {0}:: Num a_aGl[tau:0] (CDictCan)
[W] $dNum_aJO {0}:: Num b_aGm[tau:0] (CDictCan)
[W] $dNum_aJR {0}:: Num c_aGn[tau:0] (CDictCan)}
groups = [(a_aGl[tau:0],
[[W] $dNum_aJL {0}:: Num a_aGl[tau:0] (CDictCan)]),
(b_aGm[tau:0], [[W] $dNum_aJO {0}:: Num b_aGm[tau:0] (CDictCan)]),
(c_aGn[tau:0], [[W] $dNum_aJR {0}:: Num c_aGn[tau:0] (CDictCan)])]
info = ([(), [], Integer, Double], (False, True))
...
unifyTyVar a_aGl[tau:0] := Integer
writeMetaTyVar a_aGl[tau:0] := Integer
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.7.20230620:
ASSERT failed!
Double update of meta tyvar
a_aGl[tau:0]
Indirect Int
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Zonk/TcType.hs:156:10 in ghc-9.7-inplace:GHC.Tc.Zonk.TcType
writeMetaTyVarRef, called at compiler/GHC/Tc/Zonk/TcType.hs:115:5 in ghc-9.7-inplace:GHC.Tc.Zonk.TcType
writeMetaTyVar, called at compiler/GHC/Tc/Solver/Monad.hs:1306:26 in ghc-9.7-inplace:GHC.Tc.Solver.Monad
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:503:29 in ghc-9.7-inplace:GHC.Utils.Error
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```9.8.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/23816Instances with Unsatisfiable context should use unsatisfiable for missing met...2023-08-22T18:17:56Zsheafsam.derbyshire@gmail.comInstances with Unsatisfiable context should use unsatisfiable for missing methods even when they have defaultsCurrently, we only generate method implementations for instances with an `Unsatisfiable` context when they have no default implementation. However, this can cause problems, e.g.
```haskell
{-# OPTIONS_GHC -fdefer-type-errors #-}
module...Currently, we only generate method implementations for instances with an `Unsatisfiable` context when they have no default implementation. However, this can cause problems, e.g.
```haskell
{-# OPTIONS_GHC -fdefer-type-errors #-}
module T23816 where
instance Unsatisfiable (Text "Msg") => Eq (a -> b)
bad = id == id
```
calling `bad` will result in a runtime loop due to `(==)` having a default definition in terms of `(/=)` and vice-versa, when we would rather it throws the unsatisfiable type error.
The fix is to change `GHC.Tc.TyCl.Instance.tc_default` to always create an `unsatisfiable` RHS even when there is a default method. I will execute.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23784mkGADTVars panic with a GADT data family instance and unused variable in forall2024-02-08T14:23:32Zsheafsam.derbyshire@gmail.commkGADTVars panic with a GADT data family instance and unused variable in forall```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LA...```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module T23784 where
import Data.Kind
type Sing :: forall k. k -> Type
data family Sing a
data instance forall a b. Sing a where
S :: Sing '()
```
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.9.20230724:
mkGADTVars
[k_awT[sk:1], b_awF[sk:1], k_awU[sk:1], a_awE[sk:1]]
<InScope = {a_awE[sk:1] k_awU[sk:1]}
IdSubst = []
TvSubst = [awE :-> '(), awU :-> ()]
CvSubst = []>
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Panic.hs:191:37 in ghc-9.9-inplace:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Tc\TyCl.hs:4244:9 in ghc-9.9-inplace:GHC.Tc.TyCl
CallStack (from HasCallStack):
panic, called at compiler\GHC\Utils\Error.hs:503:29 in ghc-9.9-inplace:GHC.Utils.Error
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I think this is to do with the way we create a representation `TyCon` for a data family instance using the full set of bound variables in the `forall` (see the use of `ty_binders` in `mkAlgTyCon` in `GHC.Tc.TyCl.Instance.tcDataFamInstDecl` and Note [Data type families] in `GHC.Core.TyCon`).
I ran into this when working on error messages for unused type variables in family instances in !11032. I will investigate, but pinging @rae as the authority on this code (in case anything obvious springs to mind).9.10.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23778Confusing error message for unused variables in RHS of data family instance2024-02-08T14:23:33Zsheafsam.derbyshire@gmail.comConfusing error message for unused variables in RHS of data family instance```haskell
{-# LANGUAGE TypeFamilies #-}
module T23778 where
import Data.Kind
data family D :: Type
data instance forall (d :: Type). D = MkD
```
On GHC 9.6 I get
```
* Type variable `d' is mentioned in the RHS,
but not b...```haskell
{-# LANGUAGE TypeFamilies #-}
module T23778 where
import Data.Kind
data family D :: Type
data instance forall (d :: Type). D = MkD
```
On GHC 9.6 I get
```
* Type variable `d' is mentioned in the RHS,
but not bound on the LHS of the family instance
```
The message was reworded slightly in 9.8 with the error constructor migration, but it's similar:
```
* Out of scope type variable `d' in the RHS of a family instance.
All such variables must be bound on the LHS.
```
Instead I would expect to get an error that matches the one we get for type family instances
```haskell
type family F
type instance forall (a :: Type). F = ()
```
```
* Type variable `a' is bound by a forall,
but not used in the family instance.
```9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23768Check for unused type variables in type instances is buggy for associated typ...2024-02-08T14:23:32Zsheafsam.derbyshire@gmail.comCheck for unused type variables in type instances is buggy for associated type defaultsCurrently, a program like
```haskell
type family F
type instance forall a. F = ()
```
will give rise to an error
```
* Type variable `a' is bound by a forall,
but not used in the family instance.
* In the type instance...Currently, a program like
```haskell
type family F
type instance forall a. F = ()
```
will give rise to an error
```
* Type variable `a' is bound by a forall,
but not used in the family instance.
* In the type instance declaration for `F'
```
Associated type defaults go through the same logic (`checkValidClass` calls `checkValidTyFamEqn` which calls `checkFamPatBinders`), but I think it is passed incorrect arguments, which means that the following program:
```haskell
class C where
type H
type forall c. H = ()
```
does not give rise to any errors, when we would expect a similar error as above.
I will fix as part of my investigations into #23734.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23661tcVTA: untested zonk and outdated Note [Visible type application zonk]2023-08-05T08:57:23ZVladislav ZavialovtcVTA: untested zonk and outdated Note [Visible type application zonk]In `compiler/GHC/Tc/Gen/App.hs`, we have a function for type checking type applications `f @t`:
```haskell
tcVTA :: TcType -- Function type
-> LHsWcType GhcRn -- Argument type
-> TcM (TcType, TcType)
```
The fi...In `compiler/GHC/Tc/Gen/App.hs`, we have a function for type checking type applications `f @t`:
```haskell
tcVTA :: TcType -- Function type
-> LHsWcType GhcRn -- Argument type
-> TcM (TcType, TcType)
```
The first thing it does is split off the forall from the function type given to it
```haskell
tcVTA fun_ty hs_ty
| Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
, binderFlag tvb == Specified
= do { ...
...
... }
```
So if the `fun_ty` is `forall a. a -> a`, then `tvb` stands for `a` and `inner_ty` stands for `a -> a`. Quite straightforward so far.
Then, a bit further into the function definition, it zonks the `inner_ty`
```haskell
; inner_ty <- liftZonkM $ zonkTcType inner_ty
-- See Note [Visible type application zonk]
```
But why is this zonk needed? The referenced Note explains
```
Note [Visible type application zonk]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
* tcHsTypeApp only guarantees that
- ty_arg is zonked
- kind(zonk(tv)) = kind(ty_arg)
(checkExpectedKind zonks as it goes).
So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
and inner_ty. Otherwise we can build an ill-kinded type. An example was #14158,
where we had:
id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
and we had the visible type application
id @(->)
* We instantiated k := kappa, yielding
forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
Here q1 :: RuntimeRep
* Now we substitute
cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
but we must first zonk the inner_ty to get
forall (a :: TYPE q1). cat a a
so that the result of substitution is well-kinded
Failing to do so led to #14158.
-}
```
The issue is that I can't reproduce the problem described by the Note. The test case `T14158` passes even if the zonk is removed! In fact, the entire test suite passes. This could mean one of two things:
1. The zonk is not needed anymore
2. We need a better test case for the zonk
So which one it is? Depending on the answer, the solution to this ticket is either to remove the zonk or to add a new test case.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23617mkSelCo produces the wrong role2024-03-29T10:41:12ZSimon Peyton JonesmkSelCo produces the wrong roleIn GHC.Core.Coercion.mkSelCo we see
```haskell
mkSelCo_maybe cs co
= assertPpr (good_call cs) bad_call_msg $
go cs co
where
Pair ty1 ty2 = coercionKind co
go cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (...In GHC.Core.Coercion.mkSelCo we see
```haskell
mkSelCo_maybe cs co
= assertPpr (good_call cs) bad_call_msg $
go cs co
where
Pair ty1 ty2 = coercionKind co
go cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo r (getNthFromType cs ty)) <--------- Yikes!
...
```
Assigning role `r` to the returned Refl is just wrong. It should be
```haskell
go cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo (mkSelCoResRole cs r) (getNthFromType cs ty))
```
where
```haskell
mkSelCoResRole :: CoSel -> Role -> Role
-- What is the role of (SelCo cs co), if co has role 'r'?
-- It is not just 'r'!
-- c.f. the SelCo case of coercionRole
mkSelCoResRole SelForAll _ = Nominal
mkSelCoResRole (SelTyCon _ r') _ = r'
mkSelCoResRole (SelFun fs) r = funRole r fs
```
This came up when I was debugging something else, so I don't have a stand-alone reproducer.https://gitlab.haskell.org/ghc/ghc/-/issues/23591Adding a quantified constraint harms type reconstruction without a good reason2023-09-28T06:00:39ZMikolaj KonarskiAdding a quantified constraint harms type reconstruction without a good reasonGHC 9.6.2 and older. A partially minimized example
https://play.haskell.org/saved/qfYAIPzc
The quantified constraint at the bottom necessitates an addition of a type applications elsewhere, as shown in the comment in the middle, for no...GHC 9.6.2 and older. A partially minimized example
https://play.haskell.org/saved/qfYAIPzc
The quantified constraint at the bottom necessitates an addition of a type applications elsewhere, as shown in the comment in the middle, for no good reason. It looks like the quantified constraint distracts the type-checker and it forgets some type variables.
A disastrous example in the wild, which may potentially exhibit also other problems:
https://github.com/Mikolaj/horde-ad/commit/58d9301a2062fe5adc6a66ff52498a74f493920f
(compile with `cabal build --disable-optimization --allow-newer`).https://gitlab.haskell.org/ghc/ghc/-/issues/23590Similar quantified constraints cancel each other2023-08-23T10:38:58ZMikolaj KonarskiSimilar quantified constraints cancel each other[Edit: please kindly ignore, while I think this through after Simon demolished my naive understanding of constraints.]
This affects GHC 9.2.8, 9.4.5 and 9.6.2.
Here's the example: https://play.haskell.org/saved/sJujfhPD (edit: and a s...[Edit: please kindly ignore, while I think this through after Simon demolished my naive understanding of constraints.]
This affects GHC 9.2.8, 9.4.5 and 9.6.2.
Here's the example: https://play.haskell.org/saved/sJujfhPD (edit: and a simpler example without any quantifiers: https://play.haskell.org/saved/h0Pz4cUB)
Without the `, Tensor ranked` line it compiles and without the `, CRankedY2 ranked BooleanMatchesYR` line it compiles, but keeping both quantified constraints makes both unsatisfiable. It's essential that the constraints are similar, but not identical. Actually, to repro with 9.6.2, I had to made them more dissimilar. With older GHCs it was enough to swap the order of constraints in the quantified constraint's context.
The workaround for this bug is to the remove one of the quantified constraints.https://gitlab.haskell.org/ghc/ghc/-/issues/23543Promoted empty list fails to kind-check with arity 02023-07-20T19:25:05ZRyan ScottPromoted empty list fails to kind-check with arity 0Data constructors that are promoted to the kind level can be partially applied, just like any other type constructor. For instance, this kind-checks:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-...Data constructors that are promoted to the kind level can be partially applied, just like any other type constructor. For instance, this kind-checks:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
type N :: forall a. Maybe a
type N = ('Nothing :: forall a. Maybe a)
```
Note that I've given `'Nothing` an explicit `forall a. Maybe a` kind signature to ensure that `N` has arity 0. That is, `N` does not require any arguments in order to partially apply it.
While most promoted data constructors (e.g., `'Nothing`) can be partially applied this way, there is a strange exception to this rule: the promoted empty list. If you try to write this:
```hs
type L :: forall a. [a]
type L = ('[] :: forall a. [a])
```
Then it will fail to kind-check:
```
$ ghc-9.6.2 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:12:11: error: [GHC-83865]
• Expected kind ‘forall a. [a]’, but ‘'[]’ has kind ‘[k0]’
• In the type ‘('[] :: forall a. [a])’
In the type declaration for ‘L’
|
12 | type L = ('[] :: forall a. [a])
| ^^^
```
I think this should kind-check, as `'[]` is a promoted data constructor just like `'Nothing` is. My suspicion is that GHC is special-casing `'[]` applications somewhere in the typechecker, and the special code path is likely mishandling things in some way.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/23520-Wincomplete-record-updates not working since 9.62023-09-19T17:01:49ZBartłomiej Cieślar-Wincomplete-record-updates not working since 9.6## Summary
Between 9.4 and 9.6 the `-Wincomplete-record-updates` flag seems to have been removed. I was not able to find anything on that in the release notes either.
## Steps to reproduce
Try to compile this code with `-Wincomplete-r...## Summary
Between 9.4 and 9.6 the `-Wincomplete-record-updates` flag seems to have been removed. I was not able to find anything on that in the release notes either.
## Steps to reproduce
Try to compile this code with `-Wincomplete-record-updates`
```haskell
module MyLib where
data T = T1 { x :: Bool } | T2
f a = do
a { x = False }
```
in 9.4, a warning is thrown, but in 9.6 it's not9.6.3sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23512Type/data instances: require that variables on the RHS are mentioned on the LHS2023-06-20T02:06:59ZVladislav ZavialovType/data instances: require that variables on the RHS are mentioned on the LHS[GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst) restricts the scope of type and data family instances as follows:
* In type f...[GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst) restricts the scope of type and data family instances as follows:
* In type family and data family instances, require that every variable mentioned on the RHS must also occur on the LHS.
For example, here are three equivalent type instance definitions accepted today:
```haskell
type family F1 a :: k
type instance F1 Int = Any :: j -> j
type family F2 a :: k
type instance F2 @(j -> j) Int = Any :: j -> j
type family F3 a :: k
type instance forall j. F3 Int = Any :: j -> j
```
* In `F1`, `j` is implicitly quantified and it occurs only on the RHS;
* In `F2`, `j` is implicitly quantified and it occurs both on the LHS and the RHS;
* In `F3`, `j` is explicitly quantified.
As the result of the proposed change, `F1` will be rejected with an out-of-scope error, while `F2` and `F3` will continue to be accepted.Andrei BorzenkovAndrei Borzenkov