GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:16:41Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14520GHC panic (TypeInType)2019-07-07T18:16:41ZIcelandjackGHC panic (TypeInType)```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp:...```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp::kat·b·c -> kat·a·b -> kat·a·c
class SCategory kat where
sId :: Sing a -> Sing (Id::kat a a)
sComp :: Sing f -> Sing g -> Sing (Comp f g)
```
triggers a panic
```
$ ghci -ignore-dot-ghci Bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
piResultTy
k_a1KI[tau:1]
a_a1vb[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type
typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type
typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.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":"GHC panic (TypeInType)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language TypeInType, TypeFamilies, TypeOperators #-}\r\n\r\nimport Data.Kind\r\n\r\ntype a ~>> b = (a, b) -> Type\r\n\r\ndata family Sing (a::k)\r\n\r\ntype family\r\n (·) (f::a~>>b) (x::a)::b\r\n\r\nclass PCategory kat where\r\n type Id ::kat·a·a\r\n type Comp::kat·b·c -> kat·a·b -> kat·a·c\r\n\r\nclass SCategory kat where\r\n sId :: Sing a -> Sing (Id::kat a a)\r\n sComp :: Sing f -> Sing g -> Sing (Comp f g)\r\n}}}\r\n\r\ntriggers a panic\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci Bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a1KI[tau:1]\r\n a_a1vb[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type\r\n typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type\r\n typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14515"Same" higher-rank kind synonyms behave differently2019-07-07T18:16:43ZIcelandjack"Same" higher-rank kind synonyms behave differentlyAs you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL ...As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL a a
```
Let us capture `forall k2. k2 -> ..` with a kind synonym
```hs
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: forall k. k -> HRank2 Type where
HREFL :: HREFL a a
```
Works fine. Phew. Let's do the same for `forall k1. k1 -> ..`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: HRank1 (HRank2 Type) where
HREFL :: HREFL a a
```
Works fine. Phew.
“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!
```hs
data HREFL :: HRank1 (HRank1 Type) -- FAILS
data HREFL :: HRank1 (HRank2 Type) -- OK
data HREFL :: HRank2 (HRank1 Type) -- OK
data HREFL :: HRank2 (HRank2 Type) -- FAILS
```
```
$ ghci -ignore-dot-ghci /tmp/Weird.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )
/tmp/Weird.hs:8:1: error:
• These kind and type variables: (b :: k2) k2 (d :: k2)
are out of dependency order. Perhaps try this ordering:
k2 (b :: k2) (d :: k2)
• In the data type declaration for ‘HREFL’
|
8 | data HREFL :: HRank2 (HRank2 Type)
| ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude>
```
Same happens defining `HRank2` in terms of `HRank1`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = HRank1 ty
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.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":"\"Same\" higher-rank kind synonyms behave differently","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind\r\n\r\n{{{#!hs\r\n-- Different from\r\n-- HREFL :: forall k1 k2. k1 -> k2 -> Type\r\n-- \r\ndata HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nLet us capture `forall k2. k2 -> ..` with a kind synonym\r\n\r\n{{{#!hs\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: forall k. k -> HRank2 Type where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nWorks fine. Phew. Let's do the same for `forall k1. k1 -> ..`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: HRank1 (HRank2 Type) where\r\n HREFL :: HREFL a a \r\n}}}\r\n\r\nWorks fine. Phew. \r\n\r\n“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!\r\n\r\n{{{#!hs\r\ndata HREFL :: HRank1 (HRank1 Type) -- FAILS\r\ndata HREFL :: HRank1 (HRank2 Type) -- OK\r\ndata HREFL :: HRank2 (HRank1 Type) -- OK \r\ndata HREFL :: HRank2 (HRank2 Type) -- FAILS\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/Weird.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )\r\n\r\n/tmp/Weird.hs:8:1: error:\r\n • These kind and type variables: (b :: k2) k2 (d :: k2)\r\n are out of dependency order. Perhaps try this ordering:\r\n k2 (b :: k2) (d :: k2)\r\n • In the data type declaration for ‘HREFL’\r\n |\r\n8 | data HREFL :: HRank2 (HRank2 Type) \r\n | ^^^^^^^^^^\r\nFailed, 0 modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nSame happens defining `HRank2` in terms of `HRank1`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = HRank1 ty\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14507Core Lint error with Type.Reflection and pattern synonyms2019-07-07T18:16:45ZIcelandjackCore Lint error with Type.Reflection and pattern synonyms```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
impor...```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
import Type.Reflection
import Prelude
import Data.Kind
data Dict c where
Dict :: c => Dict c
data N = O | S N
foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)
foo krep rep = do
HRefl <- eqTypeRep krep (typeRepKind rep)
pure (HRefl, rep)
pattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)
pattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))
where Bloop' HRefl rep = rep
type family
SING = (res :: k -> Type) | res -> k where
-- Core Lint error disappears with this line:
SING = (TypeRep :: N -> Type)
pattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)
pattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))
where RepN tr = tr
asTypeable :: TypeRep a -> Dict (Typeable a)
asTypeable rep =
withTypeable rep
Dict
pattern TypeRep :: () => Typeable a => TypeRep a
pattern TypeRep <- (asTypeable -> Dict)
where TypeRep = typeRep
-- error
pattern SO = RepN TypeRep
```
triggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.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":"Core Lint error with Type.Reflection and pattern synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}\r\n\r\nimport Type.Reflection\r\nimport Prelude\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata N = O | S N\r\n\r\nfoo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)\r\nfoo krep rep = do\r\n HRefl <- eqTypeRep krep (typeRepKind rep)\r\n pure (HRefl, rep)\r\n\r\npattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)\r\npattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))\r\n where Bloop' HRefl rep = rep\r\n\r\ntype family \r\n SING = (res :: k -> Type) | res -> k where\r\n -- Core Lint error disappears with this line:\r\n SING = (TypeRep :: N -> Type)\r\n\r\npattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)\r\npattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))\r\n where RepN tr = tr\r\n\r\nasTypeable :: TypeRep a -> Dict (Typeable a)\r\nasTypeable rep =\r\n withTypeable rep\r\n Dict\r\n\r\npattern TypeRep :: () => Typeable a => TypeRep a\r\npattern TypeRep <- (asTypeable -> Dict)\r\n where TypeRep = typeRep\r\n\r\n-- error \r\npattern SO = RepN TypeRep\r\n}}}\r\n\r\ntriggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14394Inferred type for pattern synonym has redundant equality constraint2019-07-07T18:17:11ZRyan ScottInferred type for pattern synonym has redundant equality constraintLoad this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.o...Load this file into GHCi:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where
import Data.Type.Equality
pattern Foo = HRefl
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
```
Notice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}
module Works where
import Data.Type.Equality
pattern Foo = HRefl
```
```
λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
(b :: k2) ~~ (a :: k1)) => a :~~: b
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Inferred type for pattern synonym has redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this file into GHCi:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: 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\nOk, 1 module loaded.\r\nλ> :i Foo\r\npattern Foo :: () => (* ~ *, b ~ a) => a :~~: b\r\n}}}\r\n\r\nNotice that the type signature for `Foo` has an entirely redundant `* ~ *` constraint. The same does not happen if `TypeInType` is enabled.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Works where\r\n\r\nimport Data.Type.Equality\r\n\r\npattern Foo = HRefl\r\n}}}\r\n{{{\r\nλ> :i Foo\r\npattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,\r\n (b :: k2) ~~ (a :: k1)) => a :~~: b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14352Higher-rank kind ascription oddities2019-07-07T18:17:21ZRyan ScottHigher-rank kind ascription odditiesGHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy...GHC accepts these two definitions:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Proxy
f :: forall (x :: forall a. a -> Int). Proxy x
f = Proxy
g :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)
g = Proxy
```
However, it does not accept this one, which (AFAICT) should be equivalent to the two above:
```hs
h :: forall x. Proxy (x :: forall b. b -> Int)
h = Proxy
```
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:23: error:
• Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely
‘(x :: forall b. b -> Int)’
In the type signature:
h :: forall x. Proxy (x :: forall b. b -> Int)
|
13 | h :: forall x. Proxy (x :: forall b. b -> Int)
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"Higher-rank kind ascription oddities","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts these two definitions:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nf :: forall (x :: forall a. a -> Int). Proxy x\r\nf = Proxy\r\n\r\ng :: forall (x :: forall a. a -> Int). Proxy (x :: forall b. b -> Int)\r\ng = Proxy\r\n}}}\r\n\r\nHowever, it does not accept this one, which (AFAICT) should be equivalent to the two above:\r\n\r\n{{{#!hs\r\nh :: forall x. Proxy (x :: forall b. b -> Int)\r\nh = Proxy\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.1: 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:13:23: error:\r\n • Expected kind ‘forall b. b -> Int’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘Proxy’, namely\r\n ‘(x :: forall b. b -> Int)’\r\n In the type signature:\r\n h :: forall x. Proxy (x :: forall b. b -> Int)\r\n |\r\n13 | h :: forall x. Proxy (x :: forall b. b -> Int)\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14203GHC-inferred type signature doesn't actually typecheck2019-07-07T18:17:58ZRyan ScottGHC-inferred type signature doesn't actually typecheckThis code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * ->...This code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)
```
I was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:
```
λ> :i SMkSigma
data instance Sing z where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
x) (px :: Apply p x).
(Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)
```
I attempted to incorporate this newfound knowledge into the program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).
Sing sx -> Sing px -> Sing (MkSigma sx px)
```
But to my surprise, adding this inferred type signature causes the program to no longer typecheck!
```
GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:31: error:
• Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
• In the first argument of ‘Sing’, namely ‘px’
In the type ‘Sing px’
In the definition of data constructor ‘SMkSigma’
|
23 | Sing sx -> Sing px -> Sing (MkSigma sx px)
| ^^
```
I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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":"GHC-inferred type signature doesn't actually typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nI was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:\r\n\r\n{{{\r\nλ> :i SMkSigma\r\ndata instance Sing z where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing\r\n x) (px :: Apply p x).\r\n (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)\r\n}}}\r\n\r\nI attempted to incorporate this newfound knowledge into the program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).\r\n Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nBut to my surprise, adding this inferred type signature causes the program to no longer typecheck!\r\n\r\n{{{\r\nGHCi, version 8.3.20170907: 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:23:31: error:\r\n • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’\r\n • In the first argument of ‘Sing’, namely ‘px’\r\n In the type ‘Sing px’\r\n In the definition of data constructor ‘SMkSigma’\r\n |\r\n23 | Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n | ^^\r\n}}}\r\n\r\nI'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14042Datatypes cannot use a type family in their return kind2019-10-07T17:13:51ZRyan ScottDatatypes cannot use a type family in their return kindThis typechecks:
```hs
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Id (a :: Type) = a
data Foo :: Id Type
```
But changing the type synonym to a type family causes it to fail:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ...This typechecks:
```hs
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Id (a :: Type) = a
data Foo :: Id Type
```
But changing the type synonym to a type family causes it to fail:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
type family Id (a :: Type) :: Type where
Id a = a
data Foo :: Id Type
```
```
$ ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:9:1: error:
• Kind signature on data type declaration has non-* return kind
Id *
• In the data declaration for ‘Foo’
|
9 | data Foo :: Id Type
| ^^^^^^^^
```
That error message is wrong, since `Id * = *`. And, besides, the definition should be accepted.
EDIT: This was originally about the error message. But #14042 changes the goal of the bug to fix the behavior.https://gitlab.haskell.org/ghc/ghc/-/issues/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]2022-03-22T09:23:50ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-...(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type -> Type where
WeirdNil :: WeirdList a
WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs
-> p _ (WeirdCons x xs))
-> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p x0 t3 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p (WeirdList z) t2 xs
-> p z t1 ('WeirdCons x xs))
-> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/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 Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
-> (forall y. p x0 t0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))
-> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
24 | -> (forall (y :: Type). p _ WeirdNil)
| ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<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 | #13877 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type -> Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs\r\n -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n -> (forall y. p x0 t3 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs\r\n -> p (WeirdList z) t2 xs\r\n -> p z t1 ('WeirdCons x xs))\r\n -> p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/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 Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n -> (forall y. p x0 t0 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))\r\n -> p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64-unknown-linux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n24 | -> (forall (y :: Type). p _ WeirdNil)\r\n | ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64-unknown-linux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13913Can't apply higher-ranked kind in type family2019-07-07T18:19:30ZRyan ScottCan't apply higher-ranked kind in type familyThis code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g ...This code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g :: forall (a :: Type). a -> a) = g True
type family F2 (g :: forall (a :: Type). a -> a) :: Bool where
F2 g = g True
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’
• In the first argument of ‘F2’, namely ‘g’
In the type family declaration for ‘F2’
|
14 | F2 g = g True
| ^
```
This is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.
<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 apply higher-ranked kind in type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code doesn't typecheck due to `F2`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nf :: (forall (a :: Type). a -> a) -> Bool\r\nf g = g True\r\n\r\ntype F1 (g :: forall (a :: Type). a -> a) = g True\r\n\r\ntype family F2 (g :: forall (a :: Type). a -> a) :: Bool where\r\n F2 g = g True\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: 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:14:6: error:\r\n • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’\r\n • In the first argument of ‘F2’, namely ‘g’\r\n In the type family declaration for ‘F2’\r\n |\r\n14 | F2 g = g True\r\n | ^\r\n}}}\r\n\r\nThis is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13872Strange Typeable error message involving TypeInType2019-07-07T18:19:44ZRyan ScottStrange Typeable error message involving TypeInTypeI originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo whe...I originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
import Data.Typeable
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
f :: String
f = show $ typeOf SMkFoo
```
Fails in GHC 8.0.1, 8.0.2, and 8.2 (after applying [D3671](https://phabricator.haskell.org/D3671)) with a rather unsightly error message:
```
GHCi, version 8.3.20170624: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:19:12: error:
• No instance for (Typeable <>) arising from a use of ‘typeOf’
• In the second argument of ‘($)’, namely ‘typeOf SMkFoo’
In the expression: show $ typeOf SMkFoo
In an equation for ‘f’: f = show $ typeOf SMkFoo
|
19 | f = show $ typeOf SMkFoo
| ^^^^^^^^^^^^^
```
I'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)
<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":"Strange Typeable error message involving TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally discovered this when tinkering with #13871. This program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\nimport Data.Typeable\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n\r\nf :: String\r\nf = show $ typeOf SMkFoo\r\n}}}\r\n\r\nFails in GHC 8.0.1, 8.0.2, and 8.2 (after applying Phab:D3671) with a rather unsightly error message:\r\n\r\n{{{\r\nGHCi, version 8.3.20170624: 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:19:12: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeOf’\r\n • In the second argument of ‘($)’, namely ‘typeOf SMkFoo’\r\n In the expression: show $ typeOf SMkFoo\r\n In an equation for ‘f’: f = show $ typeOf SMkFoo\r\n |\r\n19 | f = show $ typeOf SMkFoo\r\n | ^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13790GHC doesn't reduce type family in kind signature unless its arm is twisted2019-07-07T18:20:04ZRyan ScottGHC doesn't reduce type family in kind signature unless its arm is twistedHere's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}...Here's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
-----
data N = Z | S N
data instance Sing (z :: N) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
type instance Promote N = N
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
```
Things get more interesting if you try to add this type instance at the end of this file:
```hs
type instance DemoteX (n :: N) = n
```
Now GHC will complain:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:49:34: error:
• Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
• In the type ‘n’
In the type instance declaration for ‘DemoteX’
|
49 | type instance DemoteX (n :: N) = n
| ^
```
That error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:
```hs
...
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n
```
Then the file typechecks without issue.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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":"GHC doesn't reduce type family in kind signature unless its arm is twisted","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code (inspired by Richard's musings [https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297 here]) which typechecks with GHC 8.2.1 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata SomeSing (k :: Type) where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\ntype family Promote k :: Type\r\n\r\nclass (Promote (Demote k) ~ k) => SingKind (k :: Type) where\r\n type Demote k :: Type\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\ntype family DemoteX (a :: k) :: Demote k\r\ntype instance DemoteX (a :: Type) = Demote a\r\n\r\ntype instance Promote Type = Type\r\n\r\ninstance SingKind Type where\r\n type Demote Type = Type\r\n fromSing = error \"fromSing Type\"\r\n toSing = error \"toSing Type\"\r\n\r\n-----\r\n\r\ndata N = Z | S N\r\n\r\ndata instance Sing (z :: N) where\r\n SZ :: Sing Z\r\n SS :: Sing n -> Sing (S n)\r\ntype instance Promote N = N\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n}}}\r\n\r\nThings get more interesting if you try to add this type instance at the end of this file:\r\n\r\n{{{#!hs\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nNow GHC will complain:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: 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:49:34: error:\r\n • Expected kind ‘Demote N’, but ‘n’ has kind ‘N’\r\n • In the type ‘n’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n49 | type instance DemoteX (n :: N) = n\r\n | ^\r\n}}}\r\n\r\nThat error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:\r\n\r\n{{{#!hs\r\n...\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n$(return [])\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nThen the file typechecks without issue.","type_of_failure":"OtherFailure","blocking":[]} -->https://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/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/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/12933Wrong class instance selection with Data.Kind.Type2022-08-04T22:32:56ZjulmWrong class instance selection with Data.Kind.TypeIf you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: S...If you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: SKind Type
SKiCo :: SKind Constraint
instance Show (SKind k) where
show SKiTy = "*"
show SKiCo = "Constraint"
class IKind k where
kind :: SKind k
instance IKind Constraint where
kind = SKiCo
```
Then, the main below will compile even though there is no (IKind Type) instance, and it will print "Constraint" two times,
instead of an expected "Constraint" then "\*":
```hs
main :: IO ()
main = do
print (kind::SKind Constraint)
print (kind::SKind Type)
```
And, the main below will print "\*" two times,
instead of an expected "\*" then "Constraint":
```hs
instance IKind Type where
kind = SKiTy
main :: IO ()
main = do
print (kind::SKind Type)
print (kind::SKind Constraint)
```
This can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.
Sorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Wrong class instance selection with Data.Kind.Type","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":"If you consider the following code:\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Constraint)\r\nimport Data.Kind\r\n\r\n-- | Partial singleton for a kind type.\r\ndata SKind k where\r\n SKiTy :: SKind Type\r\n SKiCo :: SKind Constraint\r\n\r\ninstance Show (SKind k) where\r\n show SKiTy = \"*\"\r\n show SKiCo = \"Constraint\"\r\n\r\nclass IKind k where\r\n kind :: SKind k\r\ninstance IKind Constraint where\r\n kind = SKiCo\r\n}}}\r\n\r\nThen, the main below will compile even though there is no (IKind Type) instance, and it will print \"Constraint\" two times,\r\ninstead of an expected \"Constraint\" then \"*\":\r\n{{{#!hs\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Constraint)\r\n print (kind::SKind Type)\r\n}}}\r\n\r\nAnd, the main below will print \"*\" two times,\r\ninstead of an expected \"*\" then \"Constraint\":\r\n{{{#!hs\r\ninstance IKind Type where\r\n kind = SKiTy\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Type)\r\n print (kind::SKind Constraint)\r\n}}}\r\n\r\nThis can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.\r\n\r\nSorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.","type_of_failure":"OtherFailure","blocking":[]} -->https://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.dev