GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:20:07Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13777Poor error message around CUSKs2019-07-07T18:20:07ZRichard Eisenbergrae@richarde.devPoor error message around CUSKsWhile typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :...While typing up [ticket:13761\#comment:137502](https://gitlab.haskell.org//ghc/ghc/issues/13761#note_137502), I came across a poor error message around CUSKs.
```
data Proxy (a :: k) = P
data S :: forall k. Proxy k -> Type where
MkS :: S (P :: Proxy Maybe)
```
produces
```
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
```
That promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Poor error message around CUSKs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["CUSKs","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While typing up comment:7:ticket:13761, I came across a poor error message around CUSKs.\r\n\r\n{{{\r\ndata Proxy (a :: k) = P\r\ndata S :: forall k. Proxy k -> Type where\r\n MkS :: S (P :: Proxy Maybe)\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n You have written a *complete user-suppled kind signature*,\r\n but the following variable is undetermined: k0 :: *\r\n Perhaps add a kind signature.\r\n Inferred kinds of user-written variables:\r\n}}}\r\n\r\nThat promised list of the kinds of user-written variables is empty. Either GHC should find something to print (like `k :: k0`, perhaps) or omit the header.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13762TypeInType is not documented in the users' guide flag reference2019-07-07T18:20:12ZRyan ScottTypeInType is not documented in the users' guide flag referenceAt least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value...At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Documentation |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeInType is not documented in the users' guide flag reference","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13761Can't create poly-kinded GADT with TypeInType enabled, but can without2019-07-07T18:20:12ZRyan ScottCan't create poly-kinded GADT with TypeInType enabled, but can withoutSurprisingly, this compiles without `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where
import Data.Kind
data T :: k -> Type where
MkT :...Surprisingly, this compiles without `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
```
But once you add `TypeInType`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
```
then it stops working!
```
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type ‘T Int’
In the definition of data constructor ‘MkT’
|
11 | MkT :: T Int
| ^^^
```
This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.
What's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:
```hs
data T (a :: k) where
MkT :: T Int
```
Then it will work with `TypeInType` enabled.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| 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":"Can't create poly-kinded GADT with TypeInType enabled, but can without","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Surprisingly, this compiles without `TypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\nmodule Works where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k -> Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nBut once you add `TypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata T :: k -> Type where\r\n MkT :: T Int\r\n}}}\r\n\r\nthen it stops working!\r\n\r\n{{{\r\nGHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:12: error:\r\n • Expected kind ‘k’, but ‘Int’ has kind ‘*’\r\n • In the first argument of ‘T’, namely ‘Int’\r\n In the type ‘T Int’\r\n In the definition of data constructor ‘MkT’\r\n |\r\n11 | MkT :: T Int\r\n | ^^^\r\n}}}\r\n\r\nThis bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.\r\n\r\nWhat's strange about this bug is that is requires that you write `T` with an explicit kind signature. If you write `T` like this:\r\n\r\n{{{#!hs\r\ndata T (a :: k) where\r\n MkT :: T Int\r\n}}}\r\n\r\nThen it will work with `TypeInType` enabled.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13674Poor error message which masks occurs-check failure2019-07-07T18:20:39ZRyan ScottPoor error message which masks occurs-check failureHere's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-...Here's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint -> * where
Dict :: a => Dict a
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
type family Lcm :: Nat -> Nat -> Nat where
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat = magic lcm
lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom
newtype GF (n :: Nat) = GF Integer
instance KnownNat n => Num (GF n) where
xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
abs = id
signum xf@(GF x) | x==0 = xf
| otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m -> GF m -> GF m
bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
```
Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a downright puzzling type error:
```
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
```
In particular, I'd like to emphasize this part:
```
• Could not deduce: m ~ Lcm m m
from the context: m ~ Lcm m m
```
Wat!? Surely, GHC can deduce `m ~ Lcm m m` from `m ~ Lcm m m`? I decided to flip on `-fprint-explicit-kinds` and see if there was some other issue lurking beneath the surface:
```
$ /opt/ghc/head/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:63:21: error:
• Couldn't match type ‘m’ with ‘Lcm m m’
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(-)’, namely ‘foo x y’
In the expression:
foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
In an equation for ‘bar’:
bar (x :: GF m) y
= foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
| ^^^^^^^
Bug.hs:63:31: error:
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
bound by a type expected by the context:
m ~ Lcm m m => GF m
at Bug.hs:63:31-85
‘m’ is a rigid type variable bound by
the type signature for:
bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
at Bug.hs:62:1-44
Expected type: GF m
Actual type: GF (Lcm m m)
• In the first argument of ‘(\\)’, namely ‘foo y x’
In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
In the second argument of ‘(-)’, namely
‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
• Relevant bindings include
y :: GF m (bound at Bug.hs:63:17)
x :: GF m (bound at Bug.hs:63:6)
bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
|
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
|
```
Well, not a whole lot changed. We now have this, slightly more specific error instead:
```
• Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
from the context: m ~ Lcm m m
```
Huh, this is flummoxing. Surely `(m :: Nat) ~~ (Lcm m m :: Nat)` ought to be the same thing as `m ~ Lcm m m`, right?https://gitlab.haskell.org/ghc/ghc/-/issues/13643Core lint error with TypeInType and TypeFamilyDependencies2019-07-07T18:20:49ZIcelandjackCore lint error with TypeInType and TypeFamilyDependenciesIn the code
```hs
{-# Language TypeFamilyDependencies #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language DataKinds #-}
{-# Language TypeInType #-}
{-# Language GADTs...In the code
```hs
{-# Language TypeFamilyDependencies #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language DataKinds #-}
{-# Language TypeInType #-}
{-# Language GADTs #-}
import Data.Kind (Type)
data Code = I
type family
Interp (a :: Code) = (res :: Type) | res -> a where
Interp I = Bool
data T :: forall a. Interp a -> Type where
MkNat :: T False
instance Show (T a) where show _ = "MkNat"
main = do
print MkNat
```
but add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #12102 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Core lint error with TypeInType and TypeFamilyDependencies","status":"New","operating_system":"","component":"Compiler","related":[12102],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the code\r\n\r\n{{{#!hs\r\n{-# Language TypeFamilyDependencies #-}\r\n{-# Language RankNTypes #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language DataKinds #-}\r\n{-# Language TypeInType #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata Code = I\r\n\r\ntype family\r\n Interp (a :: Code) = (res :: Type) | res -> a where\r\n Interp I = Bool\r\n\r\ndata T :: forall a. Interp a -> Type where\r\n MkNat :: T False\r\n\r\ninstance Show (T a) where show _ = \"MkNat\"\r\n\r\nmain = do\r\n print MkNat\r\n}}}\r\n\r\nbut add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13625GHC internal error: ‘Y’ is not in scope during type checking, but it passed t...2019-07-07T18:20:53ZMatthew PickeringGHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r...```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1cR :-> APromotionErr TyConPE]
• In the kind ‘Y’
```
Originally reported by \@mietek in #11821
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mietek |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["mietek"],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata X :: Y where Y :: X\r\n}}}\r\n\r\nThe error message is:\r\n\r\n{{{\r\nBug.hs:2:11: error: …\r\n • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1cR :-> APromotionErr TyConPE]\r\n • In the kind ‘Y’\r\n}}}\r\n\r\nOriginally reported by @mietek in #11821","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13603Can't resolve levity polymorphic superclass2019-07-07T18:21:04ZIcelandjackCan't resolve levity polymorphic superclassThis works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the...This works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the moment you add (`b :: TYPE rep`) to the last line it stops working
```hs
-- t3I7.hs:9:10-40: error: …
-- • Could not deduce (A b)
-- arising from the superclasses of an instance declaration
-- from the context: B b
-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40
-- • In the instance declaration for ‘B (a -> b)’
-- Compilation failed.
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> (b :: TYPE rep))
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't resolve levity polymorphic superclass","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works\r\n\r\n{{{#!hs\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> b)\r\n}}}\r\n\r\nbut the moment you add (`b :: TYPE rep`) to the last line it stops working\r\n\r\n\r\n{{{#!hs\r\n-- t3I7.hs:9:10-40: error: …\r\n-- • Could not deduce (A b)\r\n-- arising from the superclasses of an instance declaration\r\n-- from the context: B b\r\n-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40\r\n-- • In the instance declaration for ‘B (a -> b)’\r\n-- Compilation failed.\r\n\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> (b :: TYPE rep))\r\n}}}\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13549GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts2019-07-07T18:21:23ZRyan ScottGHC 8.2.1's typechecker rejects code generated by singletons that 8.0 acceptsI recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but...I recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1-rc1 nor HEAD do. Here is the error message you get, in its full glory:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1328:59: error:
• Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’
‘c69895866216793215480’ is untouchable
inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
Bug.hs:1328:59: error:
• Could not deduce: (Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
~~
(Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
from the context: t_a33gX ~ xs0_a33a0
bound by the type signature for:
lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
t_a33gX ~ xs0_a33a0 =>
Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply
[a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
at Bug.hs:(1122,11)-(1126,67)
or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
bound by a pattern with constructor:
SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
Sing a_11 n_a1kQc -> Sing [a_11] n_a1kQd -> Sing [a_11] z_a1kQb,
in an equation for ‘sPerms’
at Bug.hs:1143:25-36
or from: (arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f (TyFun [a_a337f] [a_a337f] -> *) ((:$) a_a337f) t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO)
bound by the type signature for:
lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
(arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f
(TyFun [a_a337f] [a_a337f] -> *)
((:$) a_a337f)
t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO) =>
Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
at Bug.hs:(1145,23)-(1152,117)
or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
The type variable ‘c69895866216793215480’ is ambiguous
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13546Kind error with type equality2019-07-07T18:21:24ZVladislav ZavialovKind error with type equalityThis code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T ...This code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T "a") ~ "a")
untt = Dict
tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict
```
fails with this error:
```
tunt.hs:17:8: error:
• Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
‘k’ is a rigid type variable bound by
the type signature for:
tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
at tunt.hs:16:1-38
When matching types
UnT (T "a") :: k
"a" :: GHC.Types.Symbol
• In the expression: Dict
In an equation for ‘tunt’: tunt = Dict
• Relevant bindings include
tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)
|
17 | tunt = Dict
|
```
Instead I would expect these reductions to take place:
```
1. T (UnT (T "a")) ~ T "a"
2. T "a" ~ T "a"
3. constraint satisfied (refl)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind error with type equality","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata T (t :: k)\r\n\r\ntype family UnT (a :: Type) :: k where\r\n UnT (T t) = t\r\n\r\nuntt :: Dict (UnT (T \"a\") ~ \"a\")\r\nuntt = Dict\r\n\r\ntunt :: Dict (T (UnT (T \"a\")) ~ T \"a\")\r\ntunt = Dict\r\n}}}\r\n\r\nfails with this error:\r\n\r\n{{{\r\ntunt.hs:17:8: error:\r\n • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’\r\n ‘k’ is a rigid type variable bound by\r\n the type signature for:\r\n tunt :: forall k. Dict T (UnT (T \"a\")) ~ T \"a\"\r\n at tunt.hs:16:1-38\r\n When matching types\r\n UnT (T \"a\") :: k\r\n \"a\" :: GHC.Types.Symbol\r\n • In the expression: Dict\r\n In an equation for ‘tunt’: tunt = Dict\r\n • Relevant bindings include\r\n tunt :: Dict T (UnT (T \"a\")) ~ T \"a\" (bound at tunt.hs:17:1)\r\n |\r\n17 | tunt = Dict\r\n | \r\n}}}\r\n\r\nInstead I would expect these reductions to take place:\r\n\r\n{{{\r\n 1. T (UnT (T \"a\")) ~ T \"a\"\r\n 2. T \"a\" ~ T \"a\"\r\n 3. constraint satisfied (refl)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13530Horrible error message due to TypeInType2019-07-07T18:21:28ZSimon Peyton JonesHorrible error message due to TypeInTypeConsider this
```
{-# LANGUAGE MagicHash, UnboxedTuples #-}
module Foo where
import GHC.Exts
g :: Int -> (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int -> (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: err...Consider this
```
{-# LANGUAGE MagicHash, UnboxedTuples #-}
module Foo where
import GHC.Exts
g :: Int -> (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int -> (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (# Int#, Int# #)
Actual type: (# Int#, Int# #)
```
What a terrible error message!! It was much better in GHC 7.10:
```
Foo.hs:11:7:
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: (# Int#, Int# #)
Actual type: (# Int#, a0 #)
```
What's going on?
The constraint solver sees
```
[W] alpha::TYPE LiftedRep ~ Int#::TYPE IntRep
```
So it homogenises the kinds, *and unifies alpha* (this did not happen in GHC 7.10), thus
```
alpha := Int# |> TYPE co
[W] co :: LiftedRep ~ IntRep
```
Of course the new constraint fails. But since we have unified alpha, when we print out the types are are unifying they both look like `(# Int#, Int# #)` (there's a suppressed cast in the second component).
I'm not sure what to do here.
(I tripped over this when debugging #13509.)https://gitlab.haskell.org/ghc/ghc/-/issues/13409Data types with higher-rank kinds are pretty-printed strangely2019-07-07T18:22:00ZRyan ScottData types with higher-rank kinds are pretty-printed strangelyFirst observed in #13399\##13409. If you define this:
```hs
data Foo :: (* -> *) -> (forall k. k -> *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
```...First observed in #13399\##13409. If you define this:
```hs
data Foo :: (* -> *) -> (forall k. k -> *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
```
This seems to imply that Foo has three visible type parameters, which isn't true at all!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| 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":"Data types with higher-rank kinds are pretty-printed strangely","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First observed in https://ghc.haskell.org/trac/ghc/ticket/13399#comment:5. If you define this:\r\n\r\n{{{#!hs\r\ndata Foo :: (* -> *) -> (forall k. k -> *)\r\n}}}\r\n\r\nand type `:i Foo` into GHCi, you get this back:\r\n\r\n{{{\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * -> *) k (c :: k)\r\n}}}\r\n\r\nThis seems to imply that Foo has three visible type parameters, which isn't true at all!","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13407Fix printing of higher-rank kinds2019-07-07T18:22:01ZRichard Eisenbergrae@richarde.devFix printing of higher-rank kindsWitness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeInType -XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: ...Witness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeInType -XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: (* -> *) -> (forall k. k -> *)
Prelude Data.Kind> :info Foo
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
-- Defined at <interactive>:3:1
```
The output from `:info` is terrible, treating `k` as a visible parameter when it isn't.
This is spun off from #13399 but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Fix printing of higher-rank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Witness this GHCi session:\r\n\r\n{{{\r\nrae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XTypeInType -XRankNTypes\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data Foo :: (* -> *) -> (forall k. k -> *)\r\nPrelude Data.Kind> :info Foo\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * -> *) k (c :: k)\r\n \t-- Defined at <interactive>:3:1\r\n}}}\r\n\r\nThe output from `:info` is terrible, treating `k` as a visible parameter when it isn't.\r\n\r\nThis is spun off from #13399 but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13399Location of `forall` matters with higher-rank kind polymorphism2020-05-21T22:48:30ZEric CrockettLocation of `forall` matters with higher-rank kind polymorphismThe following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- erro...The following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- error on this line
```
with the error
```
• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* -> *) -> k -> *`
Decl 3: `data Foo (a :: * -> *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13391PolyKinds is more permissive in GHC 82019-07-07T18:22:06ZEric CrockettPolyKinds is more permissive in GHC 8The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
``...The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
```
{-# LANGUAGE PolyKinds, GADTs #-}
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
The example does \*not\* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"PolyKinds is more permissive in GHC 8","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The docs claim that the definition in section 9.11.10\r\n\r\n{{{\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\n\"requires that `-XTypeInType` be in effect\", but this isn't the case.\r\n\r\nThe following compiles with GHC-8.0.2:\r\n\r\n{{{\r\n\r\n{-# LANGUAGE PolyKinds, GADTs #-}\r\n\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\nThe example does *not* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1). ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13364Remove checkValidTelescope2019-07-07T18:22:16ZRichard Eisenbergrae@richarde.devRemove checkValidTelescopeAll of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b ...All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b :: a) (c :: Proxy d). SameKind b d
forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
forall d. forall a (b :: a). SameKind b d
```
Despite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for *every* new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)
It might all just work! And then we can delete gobs of hairy code. Hooray!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Remove checkValidTelescope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have\r\n\r\n{{{\r\ndata SameKind :: k -> k -> Type\r\n}}}\r\n\r\nand then here are three subtly ill-scoped kinds:\r\n\r\n{{{\r\nforall a (b :: a) (c :: Proxy d). SameKind b d\r\nforall a. forall (b :: a). forall (c :: Proxy d). SameKind b d\r\nforall d. forall a (b :: a). SameKind b d\r\n}}}\r\n\r\nDespite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.\r\n\r\nWhile I am unaware of a concrete bug this all causes, it's a mess.\r\n\r\nBetter would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for ''every'' new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)\r\n\r\nIt might all just work! And then we can delete gobs of hairy code. Hooray!","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13337GHC doesn't think a type is of kind *, despite having evidence for it2019-07-07T18:22:23ZRyan ScottGHC doesn't think a type is of kind *, despite having evidence for itThe easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
b...The easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
blah x = x
```
```
$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a -> a
```
I find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!
If the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing -> "Non-Type kind"
Just Refl ->
case eqT :: Maybe (a :~: Int) of
Nothing -> "Non-Int type"
Just Refl -> "It's an Int!"
```
This exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC doesn't think a type is of kind *, despite having evidence for it","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The easiest way to illustrate this bug is this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\n\r\nblah :: forall (a :: k). k ~ Type => a -> a\r\nblah x = x\r\n}}}\r\n\r\n{{{\r\n$ ghci Foo.hs\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:8:43: error:\r\n • Expected a type, but ‘a’ has kind ‘k’\r\n • In the type signature:\r\n blah :: forall (a :: k). k ~ Type => a -> a\r\n}}}\r\n\r\nI find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!\r\n\r\nIf the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Typeable\r\n\r\nfoo :: forall k (a :: k) proxy. (Typeable k, Typeable a)\r\n => proxy a -> String\r\nfoo _ =\r\n case eqT :: Maybe (k :~: Type) of\r\n Nothing -> \"Non-Type kind\"\r\n Just Refl ->\r\n case eqT :: Maybe (a :~: Int) of\r\n Nothing -> \"Non-Int type\"\r\n Just Refl -> \"It's an Int!\"\r\n}}}\r\n\r\nThis exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12938Polykinded associated type family rejected on false pretenses2019-07-07T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to...If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12931tc_infer_args does not set in-scope set correctly2023-07-16T13:20:59Zjohnleotc_infer_args does not set in-scope set correctlyAs noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnche...As noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnchecked subst (tyVarKind tv)
```
This is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.
Note that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"tc_infer_args does not set in-scope set correctly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As noted in https://ghc.haskell.org/trac/ghc/ticket/12785#comment:6, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line\r\n{{{\r\nkind = substTyUnchecked subst (tyVarKind tv)\r\n}}}\r\n\r\nThis is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.\r\n\r\nNote that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12922Kind classes compile with PolyKinds2019-07-07T18:24:37ZMatthías Páll GissurarsonKind classes compile with PolyKindsI was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeO...I was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-}
module Main where
-- Define a Type for the natural numbers, zero and a successor
data Nat = Z | S Nat
class Addable k where
type (a :: k) + (b :: k) :: k
instance Addable Nat where
type (Z + a) = a
type (S a) + b = S (a + b)
main :: IO ()
main = putStrLn "Shouldn't this need TypeInType?"
```
(for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930)
Since according to a responder on \#haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds.
As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12766Allow runtime-representation polymorphic data families2019-07-07T18:25:14ZIcelandjackAllow runtime-representation polymorphic data familiesThis is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```This is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```8.10.1