GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-03-05T13:41:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15561TypeInType: Type error conditioned on ordering of GADT and type family defini...2022-03-05T13:41:59ZBj0rnTypeInType: Type error conditioned on ordering of GADT and type family definitionsConsider this code which successfully compiles:
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Inde...Consider this code which successfully compiles:
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a -> IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’
|
17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| 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":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a -> IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n |\r\n17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15116GHC internal error when GADT return type mentions its own constructor name2019-07-07T18:14:11ZRyan ScottGHC internal error when GADT return type mentions its own constructor nameTake the following program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc...Take the following program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• Data constructor ‘MkA’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’
|
6 | MkA :: A MkA
| ^^^
```
On GHC HEAD, however, this causes a GHC internal error:
```
$ ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [asv :-> Type variable ‘k’ = k :: *,
asw :-> Type variable ‘a’ = a :: k,
rqs :-> ATcTyCon A :: forall k. k -> *]
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’
|
6 | MkA :: A MkA
| ^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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 internal error when GADT return type mentions its own constructor name","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata A (a :: k) where\r\n MkA :: A MkA\r\n}}}\r\n\r\nOn GHC 8.4.2, this is rejected with a sensible error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • Data constructor ‘MkA’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n |\r\n6 | MkA :: A MkA\r\n | ^^^\r\n}}}\r\n\r\nOn GHC HEAD, however, this causes a GHC internal error:\r\n\r\n{{{\r\n$ ghc2/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [asv :-> Type variable ‘k’ = k :: *,\r\n asw :-> Type variable ‘a’ = a :: k,\r\n rqs :-> ATcTyCon A :: forall k. k -> *]\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n |\r\n6 | MkA :: A MkA\r\n | ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14808GHC HEAD regression: GADT constructors no longer quantify tyvars in topologic...2019-07-07T18:15:30ZRyan ScottGHC HEAD regression: GADT constructors no longer quantify tyvars in topological orderOriginally noticed in #14796. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
f...Originally noticed in #14796. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
f :: [()] -> ECC () [] ()
f = ECC @() @[] @()
```
Typechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:5: error:
• Couldn't match type ‘()’ with ‘[]’
Expected type: [()] -> ECC (() :: Constraint) [] ()
Actual type: () [] -> ECC (() :: Constraint) () []
• In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^^^^^^^^^^^^^^
Bug.hs:12:10: error:
• Expected kind ‘* -> *’, but ‘()’ has kind ‘*’
• In the type ‘()’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^
Bug.hs:12:14: error:
• Expecting one more argument to ‘[]’
Expected a type, but ‘[]’ has kind ‘* -> *’
• In the type ‘[]’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^
```
This is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (ctx :: Constraint) (f :: * -> *) a.
ctx =>
f a -> ECC ctx f a
```
In GHC HEAD, however, it's:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (f :: * -> *) a (ctx :: Constraint).
ctx =>
f a -> ECC ctx f a
```
This regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"Originally noticed in #14796. This program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC ctx f a where\r\n ECC :: ctx => f a -> ECC ctx f a\r\n\r\nf :: [()] -> ECC () [] ()\r\nf = ECC @() @[] @()\r\n}}}\r\n\r\nTypechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:5: error:\r\n • Couldn't match type ‘()’ with ‘[]’\r\n Expected type: [()] -> ECC (() :: Constraint) [] ()\r\n Actual type: () [] -> ECC (() :: Constraint) () []\r\n • In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^^^^^^^^^^^^^^\r\n\r\nBug.hs:12:10: error:\r\n • Expected kind ‘* -> *’, but ‘()’ has kind ‘*’\r\n • In the type ‘()’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^\r\n\r\nBug.hs:12:14: error:\r\n • Expecting one more argument to ‘[]’\r\n Expected a type, but ‘[]’ has kind ‘* -> *’\r\n • In the type ‘[]’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^\r\n}}}\r\n\r\nThis is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-foralls\r\nGHCi, version 8.4.0.20180209: 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, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (ctx :: Constraint) (f :: * -> *) a.\r\n ctx =>\r\n f a -> ECC ctx f a\r\n}}}\r\n\r\nIn GHC HEAD, however, it's:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -XTypeApplications -fprint-explicit-foralls\r\nGHCi, version 8.5.20180213: 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, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (f :: * -> *) a (ctx :: Constraint).\r\n ctx =>\r\n f a -> ECC ctx f a\r\n}}}\r\n\r\nThis regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11984Pattern match incompleteness / inaccessibility discrepancy2020-02-14T15:48:17ZRichard Eisenbergrae@richarde.devPattern match incompleteness / inaccessibility discrepancyConsider this module:
```hs
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module Bug where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
SSch :: Sing x -> Sin...Consider this module:
```hs
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module Bug where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
SSch :: Sing x -> Sing ('Sch x)
data instance Sing (x :: [k]) where
SNil :: Sing '[]
SCons :: Sing a -> Sing b -> Sing (a ': b)
data G a where
GCons :: G ('Sch (a ': b))
eval :: G s -> Sing s -> ()
eval GCons s =
case s of
-- SSch SNil -> undefined
SSch (SCons _ _) -> undefined
```
Upon seeing this, GHC says
```
Bug.hs:21:9: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: (SSch SNil)
```
So I uncomment the second-to-last line, inducing GHC to say
```
Bug.hs:22:16: error:
• Couldn't match type ‘a : b’ with ‘'[]’
Inaccessible code in
a pattern with constructor: SNil :: forall k. Sing '[],
in a case alternative
• In the pattern: SNil
In the pattern: SSch SNil
In a case alternative: SSch SNil -> undefined
```
Thankfully, this pattern is much rarer than it once was, but it's a bit sad that it's still possible.8.6.1