GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-12-29T18:28:30Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11962Support induction recursion2021-12-29T18:28:30ZRichard Eisenbergrae@richarde.devSupport induction recursionNow that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set...Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
-- Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
-- A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k) -- we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) -> (El a -> U) -> U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x -> El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/internal#separating-type-signatures-from-definitions).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `-XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n -- Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n -- A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k) -- we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) -> (El a -> U) -> U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x -> El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the right-hand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14420Data families should not instantiate to non-Type kinds2022-01-25T21:49:09ZRichard Eisenbergrae@richarde.devData families should not instantiate to non-Type kinds```hs
data family Any :: k -- allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
g...```hs
data family Any :: k -- allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Data families should not instantiate to non-Type kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k -- allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} -->https://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/14795Data type return kinds don't obey the forall-or-nothing rule2022-07-13T16:54:51ZRyan ScottData type return kinds don't obey the forall-or-nothing ruleOriginally noticed [here](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974). GHC accepts this:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Fo...Originally noticed [here](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974). GHC accepts this:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo :: forall a. a -> b -> Type where
MkFoo :: a -> Foo a b
```
Despite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.
The users' guide doesn't explicitly indicate that the `forall`-or-nothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [inconsistent design](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364670215), so I'm opening this ticket to track this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.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 type return kinds don't obey the forall-or-nothing rule","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally noticed [https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974 here]. GHC accepts this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo :: forall a. a -> b -> Type where\r\n MkFoo :: a -> Foo a b\r\n}}}\r\n\r\nDespite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.\r\n\r\nThe users' guide doesn't explicitly indicate that the `forall`-or-nothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364670215 inconsistent design], so I'm opening this ticket to track this.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14180Permit levity polymorphism in kinds2022-11-30T21:59:43ZDavid FeuerPermit levity polymorphism in kinds```hs
{-# language TypeInType, TypeFamilies, MagicHash #-}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an un...```hs
{-# language TypeInType, TypeFamilies, MagicHash #-}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```
If, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,
```hs
MatchInt ('I# (x :: Int#)) = '()
```
I get a different (and equally unhelpful) error message,
```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Strange/bad error message binding unboxed type variable","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# language TypeInType, TypeFamilies, MagicHash #-}\r\n\r\nimport GHC.Exts\r\n\r\ntype family MatchInt (f :: Int) :: () where\r\n MatchInt ('I# x) = '()\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n<interactive>:2:59: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching kinds\r\n k0 :: *\r\n Int# :: TYPE 'IntRep\r\n Expected kind ‘Int#’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘ 'I#’, namely ‘x’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# x)’\r\n In the type family declaration for ‘MatchInt’\r\n}}}\r\n\r\nIf, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,\r\n\r\n{{{#!hs\r\nMatchInt ('I# (x :: Int#)) = '()\r\n}}}\r\n\r\nI get a different (and equally unhelpful) error message,\r\n\r\n{{{\r\n • Expecting a lifted type, but ‘Int#’ is unlifted\r\n • In the kind ‘Int#’\r\n In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15710Should GHC accept a type signature that needs coercion quantification?2023-03-23T12:00:56ZSimon Peyton JonesShould GHC accept a type signature that needs coercion quantification?Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being...Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x
```
But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497https://gitlab.haskell.org/ghc/ghc/-/issues/20171Core Lint error around pure unifier and coercions2023-05-16T20:10:31ZRichard Eisenbergrae@richarde.devCore Lint error around pure unifier and coercionsThis ticket is closely related to #20146, #20172
If I say
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
typ...This ticket is closely related to #20146, #20172
If I say
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures,
TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind
type F :: Type -> Type
type family F k where
F k = Type -> Type
type family G a where
forall (k :: Type) (a :: F k) (b :: Type). G (a b, k) = Char
x :: G (Maybe Int, Bool)
x = 'y'
```
I get (with `-dcore-lint`)
```
*** Core Lint errors : in result of Desugar (before optimization) ***
Bug.hs:16:1: warning:
The type variable @k_auc is out of scope
In the RHS of x :: G (Maybe Int, Bool)
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
x :: G (Maybe Int, Bool)
[LclIdX]
x = (C# 'y'#)
`cast` (Sub (Sym (D:R:G[0]
<Bool>_N <(Maybe |> Sym (D:R:F[0] <k_auc>_N))>_N <Int>_N))
:: Char ~R# G (Maybe Int, Bool))
end Rec }
*** End of Offense ***
```
The problem is the `kco` parameter in the pure unifier.
When we have target: `ty1 |> co` and template: `ty2`, GHC remembers `co` as the relationship between the kinds of `ty1` and `ty2`, and then matches `ty1` against `ty2`. The problem is that this "remembered coercion" (called `kco` in the code) sometimes comes from the template (as here) and sometimes from the target. It thus mixes variables from both the template and the target.
This is addressed in Note [Matching in the presence of casts (1)] in GHC.Core.Unify. However, that Note is subtly wrong, in the presence of a type like `(a |> co) b`, which is what we have here. Specifically, we have
template variables: `k :: Type`, `a :: F k`, `b :: Type`
template: `((a |> axF[k]) b, k)`
target: `(Maybe Int, Bool)`
where `axF :: [k]. F k ~ (Type -> Type)`. (The `[k]` notation says that `k` is a parameter of the axiom.)
The matcher goes left-to-right, and thus matches `a |-> Maybe |> sym axF[k]` *before* it matches `k`. The `k` thus ends up in the final substitution, free.
Possible solutions:
1. Require the `kco` to mention only variables from the target, never the template (as today). Then, whenever the matcher sees a coercion in the template (e.g. `ty |> co`), create a fresh variable `cv` and remember the coercion spotted in the template (e.g. `co`). At the end, apply the substitution that is the result of the (successful) match to the remembered coercions, and then build a substitution mapping the fresh `cv`s to the substituted remembered `co`s. This would work, but it would perhaps need to run this process several times. Essentially, this is all about propagating the information about `k` back to an earlier point in the match.
2. Require the template and the target to have distinct sets of free variables. Then, we don't have to worry about mixing them together. At the end of a successful match, just find the fixpoint of the substitution. (This fixpoint operation already happens for two-way unification -- not one-way matching -- which is done by the same body of code. This approach might thus simplify some of the mediating between matching and unification already present.) We could choose to skip the fixpoint calculation if no coercions were encountered in the template, the vastly common case.
3. Forbid type families in the kinds of template variables (much like type families are generally forbidden in templates). Since we have no free coercion variables in templates and no type families in them either, it would seem that all coercions must be reflexive, thus sidestepping the problem. This seems delicate though, and likely not to be true forever (example: `unsafeCoerce` in types).
Right now, (2) seems most appealing.https://gitlab.haskell.org/ghc/ghc/-/issues/14668Ordering of declarations can cause typechecking to fail2023-06-30T17:10:59ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
data CInst
data G (b :: ()) = G
class C a where
type family F a
...The following will successfully typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
-- data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’
|
23 | type F' CInst (b :: F CInst) = G b
|
```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<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":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n-- data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n |\r\n23 | type F' CInst (b :: F CInst) = G b\r\n | \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12564Type family in type pattern kind2023-08-19T13:41:26ZVladislav ZavialovType family in type pattern kindI want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do ...I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:
```haskell
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}
import Data.Kind
data N = Z | S N
type family Len (xs :: [a]) :: N where
Len '[] = Z
Len (_ ': xs) = S (Len xs)
data Fin :: N -> Type where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
At (x ': _) FZ = x
At (_ ': xs) (FS i) = At xs i
```
It fails to compile with this error:
```
FinAt.hs:16:3: error:
• Illegal type synonym family application in instance: 'FZ
• In the equations for closed type family ‘At’
In the type family declaration for ‘At’
```
That's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.
I tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:
```haskell
x :: At '[Bool] FZ
x = True
```
results in
```
FinAt.hs:20:5: error:
• Couldn't match expected type ‘At
* ((':) * Bool ('[] *)) ('FZ 'Z)’
with actual type ‘Bool’
• In the expression: True
In an equation for ‘x’: x = True
```
<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, int-index |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family in type pattern kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","int-index"],"type":"Bug","description":"I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}\r\n\r\nimport Data.Kind\r\n\r\ndata N = Z | S N\r\n\r\ntype family Len (xs :: [a]) :: N where\r\n Len '[] = Z\r\n Len (_ ': xs) = S (Len xs)\r\n\r\ndata Fin :: N -> Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n -> Fin (S n)\r\n\r\ntype family At (xs :: [a]) (i :: Fin (Len xs)) :: a where\r\n At (x ': _) FZ = x\r\n At (_ ': xs) (FS i) = At xs i\r\n}}}\r\n\r\nIt fails to compile with this error:\r\n\r\n{{{\r\nFinAt.hs:16:3: error:\r\n • Illegal type synonym family application in instance: 'FZ\r\n • In the equations for closed type family ‘At’\r\n In the type family declaration for ‘At’\r\n}}}\r\n\r\nThat's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.\r\n\r\nI tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:\r\n\r\n{{{#!haskell\r\nx :: At '[Bool] FZ\r\nx = True\r\n}}}\r\n\r\nresults in\r\n\r\n{{{\r\nFinAt.hs:20:5: error:\r\n • Couldn't match expected type ‘At\r\n * ((':) * Bool ('[] *)) ('FZ 'Z)’\r\n with actual type ‘Bool’\r\n • In the expression: True\r\n In an equation for ‘x’: x = True\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13933Support Typeable instances for types with coercions2023-09-19T10:15:45ZRichard Eisenbergrae@richarde.devSupport Typeable instances for types with coercionsIf I say
```hs
{-# LANGUAGE GADTs, TypeApplications, TypeInType #-}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeab...If I say
```hs
{-# LANGUAGE GADTs, TypeApplications, TypeInType #-}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG
|
10 | rep = typeRep @MkG
|
```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeApplications, TypeInType #-}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n |\r\n10 | rep = typeRep @MkG\r\n | \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12612Allow kinds of associated types to depend on earlier associated types2023-12-22T08:53:22ZdavemenendezAllow kinds of associated types to depend on earlier associated typesGHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t -> Type
m :: t -> T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used...GHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t -> Type
m :: t -> T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t -> Type’
```
See [e-mail discussion](https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<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":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t -> Type\r\n\r\n m :: t -> T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t -> Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-September/026402.html e-mail discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12239Dependent type family does not reduce2024-02-27T13:56:52ZVladislav ZavialovDependent type family does not reduceWhen a type family is used in a kind of an argument for another type family, it does not reduce. Here's example code:
```
{-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}
import Data.Kind (Type)
data N = Z | S N
data Fin :: N -> Type...When a type family is used in a kind of an argument for another type family, it does not reduce. Here's example code:
```
{-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}
import Data.Kind (Type)
data N = Z | S N
data Fin :: N -> Type where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
type family FieldCount (t :: Type) :: N
type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type
data T
type instance FieldCount T = S (S (S Z))
type instance FieldType T FZ = Int
type instance FieldType T (FS FZ) = Bool
type instance FieldType T (FS (FS FZ)) = String
```
Unfortunately, I get these errors during typechecking:
```
[1 of 1] Compiling Main ( fieldtype.hs, fieldtype.o )
fieldtype.hs:19:27: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FZ’ has kind ‘Fin ('S n0)’
• In the second argument of ‘FieldType’, namely ‘FZ’
In the type instance declaration for ‘FieldType’
fieldtype.hs:20:28: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FS 'FZ’ has kind ‘Fin ('S ('S n0))’
• In the second argument of ‘FieldType’, namely ‘FS FZ’
In the type instance declaration for ‘FieldType’
fieldtype.hs:21:28: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FS ('FS 'FZ)’ has kind ‘Fin ('S ('S ('S n0)))’
• In the second argument of ‘FieldType’, namely ‘FS (FS FZ)’
In the type instance declaration for ‘FieldType’
```
<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":"Dependent type family does not reduce","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When a type family is used in a kind of an argument for another type family, it does not reduce. Here's example code:\r\n\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata N = Z | S N\r\n\r\ndata Fin :: N -> Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n -> Fin (S n)\r\n\r\ntype family FieldCount (t :: Type) :: N\r\n\r\ntype family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type\r\n\r\ndata T\r\n\r\ntype instance FieldCount T = S (S (S Z))\r\n\r\ntype instance FieldType T FZ = Int\r\ntype instance FieldType T (FS FZ) = Bool\r\ntype instance FieldType T (FS (FS FZ)) = String\r\n}}}\r\n\r\nUnfortunately, I get these errors during typechecking:\r\n\r\n{{{\r\n[1 of 1] Compiling Main ( fieldtype.hs, fieldtype.o )\r\n\r\nfieldtype.hs:19:27: error:\r\n • Expected kind ‘Fin (FieldCount T)’,\r\n but ‘'FZ’ has kind ‘Fin ('S n0)’\r\n • In the second argument of ‘FieldType’, namely ‘FZ’\r\n In the type instance declaration for ‘FieldType’\r\n\r\nfieldtype.hs:20:28: error:\r\n • Expected kind ‘Fin (FieldCount T)’,\r\n but ‘'FS 'FZ’ has kind ‘Fin ('S ('S n0))’\r\n • In the second argument of ‘FieldType’, namely ‘FS FZ’\r\n In the type instance declaration for ‘FieldType’\r\n\r\nfieldtype.hs:21:28: error:\r\n • Expected kind ‘Fin (FieldCount T)’,\r\n but ‘'FS ('FS 'FZ)’ has kind ‘Fin ('S ('S ('S n0)))’\r\n • In the second argument of ‘FieldType’, namely ‘FS (FS FZ)’\r\n In the type instance declaration for ‘FieldType’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Vladislav ZavialovVladislav Zavialov