GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-07-27T21:31:47Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20172Coercion prevents type family equation from applying2021-07-27T21:31:47ZRichard Eisenbergrae@richarde.devCoercion prevents type family equation from applyingGHC rejects this program:
```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
t...GHC rejects this program:
```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 family G a where
forall (k :: Type) (a :: Type -> F k) (b :: Type). G (a b, k) = Char
x :: G (Maybe Int, Bool)
x = 'y'
```
It would be accepted if the `a` were missing its kind signature in the equation for `G`.
The problem is that we end up with a template like `((a b) |> co, k)` , and GHC's matcher does not know how to propagate a coercion that casts the result of an application.
Closely related to #20146, #20171https://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/19802Pure unifier is incomplete around casts and AppTys: instance lookup fails2021-05-10T10:15:47ZRichard Eisenbergrae@richarde.devPure unifier is incomplete around casts and AppTys: instance lookup failsThe pure unifier (in `GHC.Core.Unify`) is incomplete with respect to casts. Here is the counter-example:
```
alpha :: Type -> Type -- this is the template variable
a :: Type -> k
co :: k ~ Type
(alpha Int) ~? (a Int |> co)
...The pure unifier (in `GHC.Core.Unify`) is incomplete with respect to casts. Here is the counter-example:
```
alpha :: Type -> Type -- this is the template variable
a :: Type -> k
co :: k ~ Type
(alpha Int) ~? (a Int |> co)
```
Today, the pure unifier will claim that these two types have no unifier. But they do:
```
alpha :-> a |> <Type> -> co
```
This, unfortunately, will not be easy to solve. We will have to somehow remember the casts that we see as we descend into a type, and use those casts for rewriting.
Here is a concrete program that witnesses the problem:
```hs
{-# LANGUAGE FlexibleInstances, TypeFamilies, ExplicitForAll, KindSignatures,
DataKinds #-}
module Bug where
import Data.Kind ( Type )
class C a where
meth :: a -> ()
instance C (b Int) where
meth _ = ()
type family Star where
Star = Type
f :: forall (c :: Type -> Star). c Int -> ()
f x = meth x
```
As written, it fails with
```
Bug.hs:17:7: error:
• No instance for (C (c Int)) arising from a use of ‘meth’
• In the expression: meth x
In an equation for ‘f’: f x = meth x
|
17 | f x = meth x
| ^^^^^^
```
But change the type of `c` to become `Type -> Type`, and the program is accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/19652GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check ...2021-04-08T08:48:53ZRichard Eisenbergrae@richarde.devGHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failureConsider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
im...Consider this mess:
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 -> k2 -> Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () -> Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```
GHC fails (in the RHS of `g`) with an occurs-check, but it should succeed.
The problem is that we end up with
```
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
```
where we have already unified `upsilon := '()`.
But GHC refuses to rewrite in kinds, so the `Const` never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type` and `beta := Any @Type |> sym (AxConst Type (Any @Type))`.
Proposed solution:
The wanted above actually gets simplified to become
```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)
```
The `co` is easily solved. Then, when we get to `w2`, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha` is free in `co` and reorient, giving
```
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)
```
which can be solved by unifying `beta := alpha |> sym co`. `alpha` will then remain unconstrained and will be zonked to `Any`.
The key new part is looking at the coercion when deciding whether to reorient.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/18689Why check for -fdefer-type-errors in metaTyVarUpdateOK?2020-12-22T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for -fdefer-type-errors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can f...Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/18308Order of StandaloneKindSignatures and CUSKs extensions significant2021-03-31T15:14:45ZBjörn HegerforsOrder of StandaloneKindSignatures and CUSKs extensions significant## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the...## Summary
I have some code that compiles without the `StandaloneKindSignatures` extension, does not compile with it, but does compile again if I also add the `CUSKs` extension _after_ `StandaloneKindSignatures`. However, if I place the `CUSKs` extension _before_ `StandaloneKindSignatures`, then the code doesn't compile.
I'm not sure if I can avoid a CUSK in this case either, because it revolves around an associated type family, which to my understanding stand-alone kind signatures cannot (yet) be written for.
I generally try to keep my extensions arranged alphabetically, which is unfortunate in this case. But that's not at all a big worry. For now I can put `CUSKs` after `StandaloneKindSignatures` as a workaround.
## Steps to reproduce
Boiling it down to a minimal demonstrative case, this compiles:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE CUSKs #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
but this doesn't:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE CUSKs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
import Data.Proxy (Proxy)
class Cls where
type Fam (k :: Type) (a :: k) :: Type
mtd :: Proxy k -> Proxy (a :: k) -> Fam k a -> Int
```
## Expected behavior
I would expect both of the above to compile.
I should also note that it's not very clear to me what it is about the type signature for `mtd` that makes it problematic. The part that is sensitive here is the `(a :: k)` kind annotation. Whether I instead put that annotation in a `forall` makes no difference. If I simply remove the kind annotation for `a`, and let it be inferred, the code compiles regardless of which of `StandaloneKindSignatures` and `CUSKs` are enabled (and in which order). I don't know if this part behaves as expected or not.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/18062A cast might get in the way of instantiation2020-04-27T10:20:56ZSimon Peyton JonesA cast might get in the way of instantiationSuppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kind-checks to
```
forall a. ((Eq a => Blah) |> co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) ...Suppose we have a type signature `f :: forall a. Eq a => blah`, and it somehow kind-checks to
```
forall a. ((Eq a => Blah) |> co)
```
In principle this can happen:
```
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
= do { ctxt' <- tc_hs_context mode ctxt
; ek <- newOpenTypeKind -- The body kind (result of the function) can
-- be TYPE r, for any r, hence newOpenTypeKind
; ty' <- tc_lhs_type mode rn_ty ek
; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
liftedTypeKind exp_kind }
```
That `checkExpectedKind` can add a cast.
If this happens, our instantiation mechanisms would fall over in a heap. We'd instantiate the `forall a`, but then fail to instantiate the `Eq a =>`; instead we'd unify `(Eq a => blah) |> co` with the function body. Bad, bad.
This popped up when fixing #18008, when a missing zonk in `tcHsPartialSigType` was producing just such a forall (with a Refl coercion). But it seems plausible that it could happen for real.
EDIT: And it does:
```hs
{-# LANGUAGE KindSignatures, TypeFamilies, DataKinds #-}
module Bug where
import Data.Kind ( Type )
type family Star where
Star = Type
f :: ((Eq a => a -> Bool) :: Star)
f x = x == x
```
produces
```
Bug.hs:11:1: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
Eq a :: Constraint
Expected type: Eq a => a -> Bool
Actual type: a0 -> Bool
• The equation(s) for ‘f’ have one argument,
but its type ‘Eq a => a -> Bool’ has none
• Relevant bindings include
f :: Eq a => a -> Bool (bound at Bug.hs:11:1)
|
11 | f x = x == x
| ^^^^^^^^^^^^
```
Solution: teach instantiation to look through casts.https://gitlab.haskell.org/ghc/ghc/-/issues/17674Kill EQ12021-09-17T17:18:39ZRichard Eisenbergrae@richarde.devKill EQ1Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a For...Note [Respecting definitional equality] introduces invariant EQ1:
```
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
```
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified `eqType` to look at the kind of arguments to `AppTy`s, then we wouldn't need EQ1, significantly simplifying `mkAppTy`. (Actually, it will just remove 2 lines. But it removes two calls to `decomposePiCos`. This will allow the one remaining call to this function to have more sway in the design of `decomposePiCos`, simplifying that bit of code, as well.)
Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See https://gitlab.haskell.org/ghc/ghc/issues/17644#note_245757.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17621Type-level multiplication parsed as application at kind *, no guidance provided2020-01-05T03:00:19ZGeshType-level multiplication parsed as application at kind *, no guidance provided## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set -XDataKinds -XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* ->...## Summary
Location of documentation issue: GHC error message
To reproduce:
```
Prelude> :set -XDataKinds -XTypeOperators
Prelude> import GHC.TypeNats
Prelude GHC.TypeNats> :k 2 * 4
<interactive>:1:1: error:
• Expected kind ‘* -> GHC.Types.Nat -> k0’,
but ‘2’ has kind ‘GHC.Types.Nat’
• In the type ‘2 * 4’
```
The error message is correct, but useless for someone getting started working
at the type level. At the very least, a suggestion of adding ```NoStarIsType```
is in order.
## Proposed improvements or changes
In a kinding error of form "expected ```* -> r```, found ```s```" with
```StarInType```, suggest that this error might be the due to ```StarInType```.
## Environment
* GHC version used (if appropriate): 8.6.5. Asked on IRC, and @solonarv checked
this still exists in 8.8https://gitlab.haskell.org/ghc/ghc/-/issues/17368Implement homogeneous equality2021-06-16T15:54:59ZRichard Eisenbergrae@richarde.devImplement homogeneous equalityAs observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. T...As observed in [two](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1076&context=compsci_pubs) [papers](https://richarde.dev/papers/2019/dep-roles/dep-roles.pdf), the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.
This ticket is to track this change.
Step 1: Modify the type-checker to use predicates instead of types internally. This will essentially be a glorification of `PredTree` (renamed `Pred`), and a `CtEvidence` will now store a `Pred`, not a `PredType`.
See also https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/phase2, which has much discussion.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17327Kind-checking associated types2020-02-18T16:17:45ZmniipKind-checking associated types## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{-# LANGUAGE DataKinds, PolyKinds, TypeFamil...## Summary
When kind checking associated type declarations in an `instance` declaration, the instance context seems to be ignored.
## Steps to reproduce
Minimal complete example:
```haskell
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #-}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x -- good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x -- bad
{-
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’
|
11 | type F l (D k x) = x -- bad
| ^
-}
```
## Expected behavior
The second instance should kind-check (it has better instance resolution properties than the first which is why we want it).
## Environment
Tested on GHC 8.6.5 and GHC HEADhttps://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/15589Always promoting metavariables during type inference may be wrong2019-07-07T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{-# LANGUAGE ScopedTypeVariables, Typ...Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
- We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
- In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
- If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
- Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
- Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs) -- section 6.5 to be specific.)
<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":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #-}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k -> k -> Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis] -- section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15588Panic when abusing kind inference2019-07-07T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: foral...When I say
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64-apple-darwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #-}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k -> k -> Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True -> ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64-apple-darwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://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/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/14645Allow type family in data family return kind2021-11-12T13:25:10ZRichard Eisenbergrae@richarde.devAllow type family in data family return kindGHC currently allows
```hs
data family DF1 :: k1 -> k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type -> Type`, for example.)
However, it rejects
```hs
typ...GHC currently allows
```hs
data family DF1 :: k1 -> k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type -> Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x -> TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.1-alpha1 |
| 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 type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 -> k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type -> Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x -> TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","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/14319Stuck type families can lead to lousy error messages2020-01-23T19:27:40ZDavid FeuerStuck type families can lead to lousy error messagesI first noticed this problem at the type level:
```hs
{-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
ty...I first noticed this problem at the type level:
```hs
{-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* -> *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’
|
10 | type instance G "Hi" = Maybe
| ^^^^^
```
This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity it indicates.
----
I just realized we have a similar problem at the term level:
```hs
f :: forall (s :: Symbol). Proxy s -> F s
f _ _ = undefined
```
produces
```hs
ArityError.hs:14:1: error:
• Couldn't match expected type ‘F s’ with actual type ‘p0 -> a0’
The type variables ‘p0’, ‘a0’ are ambiguous
• The equation(s) for ‘f’ have two arguments,
but its type ‘Proxy s -> F s’ has only one
• Relevant bindings include
f :: Proxy s -> F s (bound at ArityError.hs:14:1)
|
14 | f _ _ = undefined
| ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s -> F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.