GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-09-07T14:37:54Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20318GHC complains about impredicativity in type synonym for a quantified constraint2021-09-07T14:37:54ZRichard Eisenbergrae@richarde.devGHC complains about impredicativity in type synonym for a quantified constraintIf I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps yo...If I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps you intended to use ImpredicativeTypes
• In the type synonym declaration for ‘T’
|
5 | type T b = (Ord b, forall a. Eq a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note that `T` defines a *constraint* synonym, not a type synonym. Accordingly, `QuantifiedConstraints` should be enough to accept this definition.
Inspired by https://mail.haskell.org/pipermail/haskell-cafe/2021-August/134388.htmlhttps://gitlab.haskell.org/ghc/ghc/-/issues/15416Higher rank types in pattern synonyms2021-09-07T15:20:48ZmniipHigher rank types in pattern synonyms```hs
{-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r -> (a -> r) -> r
pattern N <- ((\f -> f Nothing Just) -> Nothing) where N = \n...```hs
{-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-}
```
Consider the following two pattern synonyms:
```hs
pattern N :: () => () => forall r. r -> (a -> r) -> r
pattern N <- ((\f -> f Nothing Just) -> Nothing) where N = \n j -> n
pattern J :: a -> forall r. r -> (a -> r) -> r
pattern J x <- ((\f -> f Nothing Just) -> Just x) where J x = \n j -> j x
```
The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.
Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:
```hs
fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a
fooVPEqns ((\f -> f Nothing Just) -> Nothing) = Nothing
fooVPEqns ((\f -> f Nothing Just) -> Just x) = Just x
fooVPCase v = case v of
((\f -> f Nothing Just) -> Nothing) -> Nothing
((\f -> f Nothing Just) -> Just x) -> Just x
fooPSEqns N = Nothing
fooPSEqns (J x) = Just x
fooPSCase v = case v of
N -> Nothing
J x -> Just x
```
Three of these compile and work fine, the fourth breaks:
```hs
QuantPatSyn.hs:22:9: error:
• Couldn't match expected type ‘r0 -> (a -> r0) -> r0’
with actual type ‘forall r. r -> (a0 -> r) -> r’
• In the pattern: N
In a case alternative: N -> Nothing
In the expression:
case v of
N -> Nothing
J x -> Just x
• Relevant bindings include
v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a
(bound at QuantPatSyn.hs:21:1)
|
22 | N -> Nothing
| ^
QuantPatSyn.hs:23:9: error:
• Couldn't match expected type ‘r0 -> (a -> r0) -> r0’
with actual type ‘forall r. r -> (a -> r) -> r’
• In the pattern: J x
In a case alternative: J x -> Just x
In the expression:
case v of
N -> Nothing
J x -> Just x
• Relevant bindings include
v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11)
fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a
(bound at QuantPatSyn.hs:21:1)
|
23 | J x -> Just x
| ^^^
```
The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.
Another symptom can be observed with the following:
```hs
pattern V :: Void -> (forall r. r)
pattern V x <- ((\f -> f) -> x) where V x = absurd x
barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) -> Void
barVPEqns ((\f -> f) -> x) = x
barVPCase v = case v of
((\f -> f) -> x) -> x
barPSEqns (V x) = x
barPSCase v = case v of
V x -> x
```
```hs
QuantPatSyn.hs:43:9: error:
• Cannot instantiate unification variable ‘r0’
with a type involving foralls: forall r. r
GHC doesn't yet support impredicative polymorphism
• In the pattern: V x
In a case alternative: V x -> x
In the expression: case v of { V x -> x }
|
43 | V x -> x
| ^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| 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":"Higher rank types in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-}\r\n}}}\r\nConsider the following two pattern synonyms:\r\n\r\n{{{#!hs\r\npattern N :: () => () => forall r. r -> (a -> r) -> r\r\npattern N <- ((\\f -> f Nothing Just) -> Nothing) where N = \\n j -> n\r\n\r\npattern J :: a -> forall r. r -> (a -> r) -> r\r\npattern J x <- ((\\f -> f Nothing Just) -> Just x) where J x = \\n j -> j x\r\n}}}\r\n\r\nThe pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket.\r\n\r\nNow consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`:\r\n\r\n{{{#!hs\r\nfooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a\r\n\r\nfooVPEqns ((\\f -> f Nothing Just) -> Nothing) = Nothing\r\nfooVPEqns ((\\f -> f Nothing Just) -> Just x) = Just x\r\n\r\nfooVPCase v = case v of\r\n\t((\\f -> f Nothing Just) -> Nothing) -> Nothing\r\n\t((\\f -> f Nothing Just) -> Just x) -> Just x\r\n\r\nfooPSEqns N = Nothing\r\nfooPSEqns (J x) = Just x\r\n\r\nfooPSCase v = case v of\r\n\tN -> Nothing\r\n\tJ x -> Just x\r\n}}}\r\n\r\nThree of these compile and work fine, the fourth breaks:\r\n{{{#!hs\r\nQuantPatSyn.hs:22:9: error:\r\n • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’\r\n with actual type ‘forall r. r -> (a0 -> r) -> r’\r\n • In the pattern: N\r\n In a case alternative: N -> Nothing\r\n In the expression:\r\n case v of\r\n N -> Nothing\r\n J x -> Just x\r\n • Relevant bindings include\r\n v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n |\r\n22 | N -> Nothing\r\n | ^\r\n\r\nQuantPatSyn.hs:23:9: error:\r\n • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’\r\n with actual type ‘forall r. r -> (a -> r) -> r’\r\n • In the pattern: J x\r\n In a case alternative: J x -> Just x\r\n In the expression:\r\n case v of\r\n N -> Nothing\r\n J x -> Just x\r\n • Relevant bindings include\r\n v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11)\r\n fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a\r\n (bound at QuantPatSyn.hs:21:1)\r\n |\r\n23 | J x -> Just x\r\n | ^^^\r\n}}}\r\n\r\nThe exact wording of the error message (the appearance of `forall` in the \"actual type\") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly.\r\n\r\nAnother symptom can be observed with the following:\r\n\r\n{{{#!hs\r\npattern V :: Void -> (forall r. r)\r\npattern V x <- ((\\f -> f) -> x) where V x = absurd x\r\n\r\nbarVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) -> Void\r\n\r\nbarVPEqns ((\\f -> f) -> x) = x\r\n\r\nbarVPCase v = case v of\r\n\t((\\f -> f) -> x) -> x\r\n\r\nbarPSEqns (V x) = x\r\n\r\nbarPSCase v = case v of\r\n\tV x -> x\r\n}}}\r\n{{{#!hs\r\nQuantPatSyn.hs:43:9: error:\r\n • Cannot instantiate unification variable ‘r0’\r\n with a type involving foralls: forall r. r\r\n GHC doesn't yet support impredicative polymorphism\r\n • In the pattern: V x\r\n In a case alternative: V x -> x\r\n In the expression: case v of { V x -> x }\r\n |\r\n43 | V x -> x\r\n | ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/14873The well-kinded type invariant (in TcType)2021-09-07T15:47:33ZRyan ScottThe well-kinded type invariant (in TcType)(Originally noticed [here](https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTyp...(Originally noticed [here](https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a -> a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type -> Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type -> Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x -> Sing y -> Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64-unknown-linux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] |> <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travis-ci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a -> a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type -> Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type -> Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x -> Sing y -> Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180201 for x86_64-unknown-linux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] |> <*>_N)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->9.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15596When a type application cannot be applied to an identifier due to the absence...2021-09-07T15:54:40ZkindaroWhen a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Com...Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 -> a0 -> a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer
|
6 | g = f @Integer
| ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{-# language TypeApplications #-}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 -> a0 -> a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n |\r\n6 | g = f @Integer\r\n | ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15621Error message involving type families points to wrong location2021-09-07T15:55:20ZRyan ScottError message involving type families points to wrong locationConsider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~:...Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
|
12 | a = Refl
| ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let {- a :: F Int :~: F Int
a = Refl -}
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()
|
15 | b = Refl
| ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| 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":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a non-injective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n |\r\n12 | a = Refl\r\n | ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let {- a :: F Int :~: F Int\r\n a = Refl -}\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a non-injective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n |\r\n15 | b = Refl\r\n | ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/12369data families shouldn't be required to have return kind *, data instances should2021-09-09T23:17:59ZEdward Kmettdata families shouldn't be required to have return kind *, data instances shouldI'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1...I'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1: error:
• Kind signature on data type declaration has non-* return kind
(k -> *) -> k
• In the data family declaration for ‘Fix’
```
Ultimately I think the issue here is that data __instances__ should be required to end in kind \*, not the families, but this generalization didn't mean anything until we had `PolyKinds`.
As an example of a usecase, with the above, I could define a bifunctor fixed point such as
```hs
newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| 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":"data families shouldn't be required to have return kind *, data instances should","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'd like to be able to define\r\n\r\n{{{#!hs\r\n{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}\r\ndata family Fix :: (k -> *) -> k\r\nnewtype instance Fix f = In { out :: f (Fix f) }\r\n}}}\r\n\r\nBut currently this is disallowed:\r\n\r\n{{{\r\nFix.hs:2:1: error:\r\n • Kind signature on data type declaration has non-* return kind\r\n (k -> *) -> k\r\n • In the data family declaration for ‘Fix’\r\n}}}\r\n\r\nUltimately I think the issue here is that data __instances__ should be required to end in kind *, not the families, but this generalization didn't mean anything until we had `PolyKinds`.\r\n\r\nAs an example of a usecase, with the above, I could define a bifunctor fixed point such as\r\n\r\n{{{#!hs\r\nnewtype instance Fix f a = In2 { out2 :: f (Fix f a) a }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14422{-# complete #-} should be able to be at least partially type directed2021-09-16T13:34:34ZEdward Kmett{-# complete #-} should be able to be at least partially type directedThe fact that `{-# complete #-}` pragma that was added in #8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share...The fact that `{-# complete #-}` pragma that was added in #8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{-# complete (:<), Empty #-}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `-Wno-incomplete-patterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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":"{-# complete #-} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{-# complete #-}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{-# complete (:<), Empty #-}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `-Wno-incomplete-patterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/8779Exhaustiveness checks for pattern synonyms2021-09-16T13:34:34ZJoachim Breitnermail@joachim-breitner.deExhaustiveness checks for pattern synonymsPattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
Another missing pie...Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
Another missing piece is exhaustiveness checks. Given this pattern
```hs
initLast [] = Nothing
initLast xs = Just (init xs, last xs)
pattern xs ::: x <- (initLast -> Just (xs,x))
```
we want the compiler to tell the programmer that
```hs
f [] = ...
f (xs ::: x) = ...
```
is complete, while
```hs
g (xs ::: x) = ...
```
is not.
With view pattern directly, this is impossible. But the programmer did not write view patterns!
So here is what I think might work well, inspired by the new `MINIMAL` pragma:
We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.
```hs
{-# COMPLETE_PATTERNS [] && (:::) #-}
```
Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors.
When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`.
Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement.Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/301GADT constructor constraints ignored2021-09-24T11:49:26Zwolfram_kahlGADT constructor constraints ignored```
Class constraints on GADT constructore appear to be
ignored.
I tried:
data Expr :: * -> * where
Const :: Show a => a -> Expr a
Apply :: Fct a b -> Expr a -> Expr b
and there is no way to define the expected constraint-less
Sho...```
Class constraints on GADT constructore appear to be
ignored.
I tried:
data Expr :: * -> * where
Const :: Show a => a -> Expr a
Apply :: Fct a b -> Expr a -> Expr b
and there is no way to define the expected constraint-less
Show instance --- for details, see Expr0.lhs.
```6.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/20408Make `eqTypeIO` that sees through type families2021-10-04T05:42:12ZZiyang Liuunsafefixio@gmail.comMake `eqTypeIO` that sees through type families<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## Motivation
In my experience, the fact that `eqType` only sees through type synonyms, but not type families, severely limits its usefulness.
It _seems_ that it should be possible to implement `eqTypeIO` that sees through type families, via `rewrite_fam_app` and `runTcInteractive`, although I haven't studied the details.
The type would be something like `eqTypeIO :: HscEnv -> Type -> Type -> IO Bool` (or a different monad, if `IO` is not a good fit).
## Proposal
Implement `eqTypeIO`, if possible.https://gitlab.haskell.org/ghc/ghc/-/issues/20447Assert that we don't try to look up an Id too early (Occurrence is GlobalId, ...2021-10-04T13:07:19Zsheafsam.derbyshire@gmail.comAssert that we don't try to look up an Id too early (Occurrence is GlobalId, but binding is LocalId)It is not always OK to look up the `IdInfo` of an `Id` in the presence of `hs-boot` files. An example test case is `T10083`: if one tries to inspect `IdInfo`s early on in the typechecker (e.g. in the `GHC.Tc.Gen` namespace), one can get ...It is not always OK to look up the `IdInfo` of an `Id` in the presence of `hs-boot` files. An example test case is `T10083`: if one tries to inspect `IdInfo`s early on in the typechecker (e.g. in the `GHC.Tc.Gen` namespace), one can get a `Occurrence is GlobalId, but binding is LocalId` Core Lint error.
@simonpj diagnoses the problem in https://gitlab.haskell.org/ghc/ghc/-/issues/20200#note_378625:
> We have:
>
> * `T10083.hs-boot`, which defines `eqRSR`
> * `T10083a.hs`, which defines `eqSR`, whose RHS mentions `eqRSR`
> * `T10083.hs`, which defines `eqRSR`, whose RHS mentions `eqSR`.
>
> Now when compiling T10083.hs,
>
> * we typecheck the defn of `eqRSR`
> * so we need the Id (and hence Type) for `eqSR`
> * but `eqSR`'s unfolding mentions `eqRSR`, whose Id doesn't yet exist, because we havn't typechecked it.
>
> If we aggressively suck in that unfolding for `eqSR`, we'll be forced to find an Id for `eqRSR`; since it hasn't yet been built, we'll get it from the Iface from the hs-boot file ... a GlobalId. And that is the problem.
>
> Supppose we *have* finished typechecking and *now* we force that unfolding. How come we now get the typechecked defn of the Id? Answer: see GHC.IfaceToCore.tcIfaceGlobal:
>
> * It looks in `if_rec_types env` to get an IO action `get_type_env`
> * That in turn reads a ref-cell which contains the bindings for locally-defined Ids. (These will be LocalIds.
> * Somehow we update the ref-cell after typechecking. I can't see exactly where that happens. There is a maze of twisty little passages concerning `KnotVars`, and my brain exploded.
> * But if we read that ref-cell too early it'll be empty.
> * And so `tcIfaceGlobal` will look in the Iface for the hi-boot file instead.
>
> Or something like that.
Simon recommends adding an assertion to ensure we don't accidentally look up `IdInfo`s too early:
> I think that in `tcIfaceGlobal` if `cur_mod` = `nameModule name` then we should jolly well get a hit in `if_rec_types`; if not, fail with an error saying you have read `if_rec_types` too early. Or... hmm.... maybe A.hs-boot has exported something that A.hs doesn't actually define... that might happen too.
This ticket tracks this task.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/19522Levity monomorphic instantiation of unsafeCoerce# is rejected as being levity...2021-10-11T08:15:50ZRyan ScottLevity monomorphic instantiation of unsafeCoerce# is rejected as being levity polymorphic in 9.0+While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> ...While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> Int
f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
```
Surprisingly, GHC 9.0 and later reject this:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:7: error:
Cannot use function with levity-polymorphic arguments:
unsafeCoerce# :: forall (q :: RuntimeRep) (r :: RuntimeRep)
(a :: TYPE q) (b :: TYPE r).
a -> b
(Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
are eta-expanded internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Levity-polymorphic arguments: a :: TYPE q
|
10 | f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
| ^^^^^^^^^^^^^
```
The error message confuses me, since nothing about this is levity polymorphic.
Note that this only occurs if visible type applications are used. If I remove them:
```hs
f :: Int -> Int
f x = unsafeCoerce# x
```
Then GHC accepts it.9.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/19668Exponential blowup in T9198 (regresssion from 8.10 and 9.0)2021-10-11T08:17:53ZvdukhovniExponential blowup in T9198 (regresssion from 8.10 and 9.0)## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head t...## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head the cost doubles with every term, as reported in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4890#note_343948
## Steps to reproduce
Compile `testsuite/tests/perf/compiler/T9198.hs` with `+RTS -s` with varying numbers of additional `a` continuation terms. The GHC runtime and memory allocation grow exponentially. The same is not observed with GHC 8.10.4 for example.
## Expected behavior
Linear cost. With 8.10.4 and the continuation count unmodified I get:
```
$ ghc -O -fasm testsuite/tests/perf/compiler/T9198.hs +RTS -s
116,102,480 bytes allocated in the heap
...
MUT time 0.069s ( 0.572s elapsed)
GC time 0.111s ( 0.111s elapsed)
Total time 0.181s ( 0.689s elapsed)
```
With head I get:
```
514,989,696 bytes allocated in the heap
...
MUT time 0.212s ( 0.604s elapsed)
GC time 0.366s ( 0.366s elapsed)
Total time 0.581s ( 0.979s elapsed)
```
## Environment
* GHC version used: head (9.1.20210402)9.2.1Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/18704GHC could not deduce constraint from itself2021-10-14T08:52:11ZrybochodonezzarGHC could not deduce constraint from itself## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynon...## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #-}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x -> L1 c f xs -> L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) -> * where
(:*:) :: f1 x -> f2 y -> (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) -> e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s -> t a -> Foo t xs -> Foo t (s '::: a ': xs)
pattern Foo p t xs <- LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghc-bug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)-(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:45-61
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
|
38 | Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
| ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly-2020-09-14
Optional:
* Operating System: Ubuntu
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/20396Backpack does not support -ddump-tc-trace2021-10-14T09:21:15Zsheafsam.derbyshire@gmail.comBackpack does not support -ddump-tc-traceWhile working on !6164 I have needed to debug the typechecker in backpack specific scenarios, and it has been a bit of a nightmare because there is no way to enable `-ddump-tc-trace` when compiling `.bkp` files using `--backpack`.While working on !6164 I have needed to debug the typechecker in backpack specific scenarios, and it has been a bit of a nightmare because there is no way to enable `-ddump-tc-trace` when compiling `.bkp` files using `--backpack`.https://gitlab.haskell.org/ghc/ghc/-/issues/18196Type synonym lost with GADTs2021-10-17T13:38:04ZIdentical SnowflakeType synonym lost with GADTsConsider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a -> a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected ...Consider the following:
```haskell
type Joules = Double
type Grams = Double
data Unit a where
Energy :: Unit Joules
Mass :: Unit Grams
test :: Unit a -> a
test Energy = _
```
GHC reports the hole as `_ :: Double`, but I expected the synonym to remain intact, i.e., that the hole would be `_ :: Joules`.https://gitlab.haskell.org/ghc/ghc/-/issues/20277Representation-polymorphic unboxed sum causes a panic2021-10-18T10:52:12Zsheafsam.derbyshire@gmail.comRepresentation-polymorphic unboxed sum causes a panicThe existing representation-polymorphism checks allow some unboxed sums to slip through the cracks:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples #-}
mo...The existing representation-polymorphism checks allow some unboxed sums to slip through the cracks:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnboxedTuples #-}
module RepPolySum where
import GHC.Exts
baz :: forall (rep :: RuntimeRep) (a :: TYPE rep). () -> (# Int# | a #)
baz _ = (# 17# | #)
```
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
runtimeRepPrimRep
typePrimRep (a_aCt :: TYPE rep_aCs)
rep_aCs
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler\\GHC\\Types\\RepType.hs:527:5 in ghc:GHC.Types.RepType
```
(That's with GHC 9.0; the same error exists on HEAD.)
It wouldn't be hard to fix with the existing mechanisms (in the desugarer), but I'm currently fixing it in the typechecker as part of !6164.https://gitlab.haskell.org/ghc/ghc/-/issues/20330Representation-polymorphism checks for primops check too many arguments2021-10-18T10:52:12Zsheafsam.derbyshire@gmail.comRepresentation-polymorphism checks for primops check too many argumentsThe following program is currently rejected:
```haskell
blart :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
blart = raise# 5
```
```
error:
Cannot use function with representation-polymorphic arguments:
raise# :: Integer ...The following program is currently rejected:
```haskell
blart :: forall (r :: RuntimeRep) (a :: TYPE r). a -> a
blart = raise# 5
```
```
error:
Cannot use function with representation-polymorphic arguments:
raise# :: Integer -> a -> a
(Note that representation-polymorphic primops,
such as 'coerce' and unboxed tuples, are eta-expanded
internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Representation-polymorphic arguments: a :: TYPE r
|
13 | blart = raise# 5
| ^^^^^^
```
The problem is that the code that checks for disallowed representation-polymorphism when instantiating primops, which is supposed to catch cases like:
```haskell
foo :: forall (r :: RuntimeRep) (a :: TYPE r) b. a -> b
foo = unsafeCoerce#
```
ends up checking all the function arguments in the return type, even past the primop's arity.
I will be fixing this as part of !6164.https://gitlab.haskell.org/ghc/ghc/-/issues/20133Backpack can end up confused when a non-nullary type synonym implements abstr...2021-10-19T10:34:45Zsheafsam.derbyshire@gmail.comBackpack can end up confused when a non-nullary type synonym implements abstract dataGHC seems to get confused with the following `.bkp` backpack file modified from test case `T13955` in which an argument is added to the `Rep` declaration:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Dat...GHC seems to get confused with the following `.bkp` backpack file modified from test case `T13955` in which an argument is added to the `Rep` declaration:
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
unit number-unknown where
signature NumberUnknown where
import GHC.Types
data Rep a :: RuntimeRep
data Number a :: TYPE (Rep a)
plus :: Number a -> Number a -> Number a
multiply :: Number a -> Number a -> Number a
module NumberStuff where
import NumberUnknown
funcA :: Number a -> Number a -> Number a
funcA x y = plus x (multiply x y)
unit number-unboxed-int where
module NumberUnknown where
import GHC.Types
import GHC.Prim
type Rep a = IntRep
type Number a = Int#
plus :: Int# -> Int# -> Int#
plus = (+#)
multiply :: Int# -> Int# -> Int#
multiply = (*#)
unit main where
dependency number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown]
module Main where
import NumberStuff
import GHC.Types
main = print (I# (funcA 2# 3#))
```
Compiled with `ghc T20133.bkp --backpack`, we get the error:
```
T13955b.bkp:15:14: error:
* Expected kind `k0 -> *',
but `Number' has kind `TYPE 'GHC.Types.IntRep'
* In the type signature: funcA :: Number a -> Number a -> Number a
|
15 | funcA :: Number a -> Number a -> Number a
| ^^^^^^^^
T13955b.bkp:15:26: error:
* Expected kind `k0 -> *',
but `Number' has kind `TYPE 'GHC.Types.IntRep'
* In the type signature: funcA :: Number a -> Number a -> Number a
|
15 | funcA :: Number a -> Number a -> Number a
| ^^^^^^^^
T13955b.bkp:15:38: error:
* Expected kind `k0 -> *',
but `Number' has kind `TYPE 'GHC.Types.IntRep'
* In the type signature: funcA :: Number a -> Number a -> Number a
|
15 | funcA :: Number a -> Number a -> Number a
| ^^^^^^^^
```
It looks like GHC gets confused when typechecking `main` (indeed, commenting it out prevents the error); so the line numbers should be understood as referring to the instantiation of the `NumberUnknown` signature.
This is what `-ddump-tc-trace` looks like starting from there:
```
[3 of 3] Processing main
Instantiating main
[1 of 1] Including number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown]
Instantiating number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown]
[1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing ) [Source file changed]
checkHsigIface
[ryc :-> Identifier `multiply', ryd :-> Identifier `plus',
rye :-> Type constructor `Number', ryf :-> Type constructor `Rep',
ryg :-> Identifier `number-unboxed-int:NumberUnknown.$trModule',
ryU :-> Identifier `number-unboxed-int:NumberUnknown.$tcNumber',
ryV :-> Identifier `number-unboxed-int:NumberUnknown.$tcRep']
[]
[multiply, plus, Number{Number}, Rep{Rep}]
[2 of 2] Compiling NumberStuff ( number-unknown\NumberStuff.hs, nothing ) [Source file changed]
Adding diagnostic:
testsuite\tests\backpack\should_run\T13955b.bkp:13:3:
Module `Prelude' implicitly imported
checkFamInstConsistency [Prelude, NumberUnknown]
Tc2 (src)
Tc3
tcExtendKindEnvList []
tcExtendKindEnvList []
tcDeriving []
rnd
Adding instances:
Tc3b
Tc3c
tcSemigroupWarnings
Tc4
Tc4a
Tc5
tcExtendKindEnvList []
tcHsSigType { Number a_ayY -> Number a_ayY -> Number a_ayY
pushLevelAndSolveEqualitiesX { Called from tc_lhs_sig_type
newAnonMetaTyVar t_az1[tau:1]
pushLevelAndCaptureConstraints { 2
newMetaKindVar k_az2[tau:2]
bindImplicitTKBndrsX
[a_ayY]
[a_ayY[sk:2]]
tc_extend_local_env
[(a_ayY, Type variable `a_ayY' = a_ayY[sk:2] :: k_az2[tau:2])]
tcExtendBinderStack [a_ayY a_ayY[sk:2]]
newAnonMetaTyVar t_az3[tau:2]
newAnonMetaTyVar t_az4[tau:2]
lk1 Number
tcInferTyApps {
Number
[HsValArg a_ayY]
newMetaKindVar k_az5[tau:2]
newMetaKindVar k_az6[tau:2]
u_tys
tclvl 2
TYPE 'GHC.Types.IntRep ~ k_az5[tau:2] -> k_az6[tau:2]
a type equality[True] TYPE 'GHC.Types.IntRep
~
k_az5[tau:2] -> k_az6[tau:2]
```
We see here that GHC gets confused about the kind of `Number` (it thinks `Number :: TYPE IntRep`, somehow ignoring that `Number` takes an argument), and it all goes downhill from there.
Sorry for the ticket title, I didn't really know how to summarise the issue. I'm not very familiar with backpack, so I apologise if I made an elementary error somewhere.https://gitlab.haskell.org/ghc/ghc/-/issues/20356Constraint-vs-Type causes a panic2021-10-22T17:00:34ZRichard Eisenbergrae@richarde.devConstraint-vs-Type causes a panic@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type inst...@monoidal observes in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_375240 that
```hs
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds #-}
import GHC.Types
type family Id (a :: k -> Constraint) :: l -> Constraint
type instance Id f = f
type T :: Constraint -> Constraint
type T = Id Eq
data Proxy p = MkProxy
id' :: f a -> f a
id' x = x
z = id' (MkProxy @T)
```
causes
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.3.20210824:
ASSERT failed!
Ill-kinded update to meta tyvar
a_aIJ[tau:1] :: Constraint -> Constraint
Constraint -> Constraint := Eq :: * -> Constraint
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1009:10 in ghc:GHC.Tc.Utils.TcMType
```
when assertions are enabled (e.g. a `DEBUG` compiler).
Constraint-vs-Type is a difficult problem (see #11715), but I think we can pull this off and fix it. I imagine we just need to change an `eqType` to `tcEqType` somewhere.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev