GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-09-06T11:25:10Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/22144GHC accepts ambiguous type2022-09-06T11:25:10ZOleg GrenrusGHC accepts ambiguous type```haskell
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, PolyKinds, ConstraintKinds, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
i...```haskell
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, PolyKinds, ConstraintKinds, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
import Data.Kind (Constraint)
class ElimList (c :: k -> Constraint) (l :: [k]) where
elimList :: f '[] -> (forall (x :: k) (xs :: [k]). c x => ElimList c xs => f xs -> f (x : xs)) -> f l
```
GHC-9.0, 9.2 and 9.4 accept the following, GHC-8.10 and previous doens't.
The type is ambiguous, as `c` can vary. It's made clear if we want to define instances for that class:
```haskell
instance ElimList c '[] where
elimList fNil _ = fNil
instance (c x, ElimList c xs) => ElimList c (x : xs) where
elimList fNil fCons = fCons (elimList fNil fCons)
```
the nil case is fine, but the recursive case (as all other use-sites of `elimList`) fail with
```
Ambiguous.hs:15:34: error:
• Could not deduce (ElimList c0 xs)
arising from a use of ‘elimList’
```
and have to be "fixed" by using type-applications:
```haskell
instance (c x, ElimList c xs) => ElimList c (x : xs) where
elimList fNil fCons = fCons (elimList @_ @c fNil fCons)
```
(first argument is `k`).https://gitlab.haskell.org/ghc/ghc/-/issues/22141GHC-9.4 accepts "data" in kinds without DataKinds2023-11-18T13:08:29ZOleg GrenrusGHC-9.4 accepts "data" in kinds without DataKinds```haskell
import GHC.TypeLits (Nat)
import Data.Kind (Type)
data Vector :: Nat -> Type -> Type where
```
is accepted by GHC-9.4 with just `-XHaskell2010 -XGADTSyntax -XKindSignatures`. GHC-9.2 and older require `DataKinds`. I cannot f...```haskell
import GHC.TypeLits (Nat)
import Data.Kind (Type)
data Vector :: Nat -> Type -> Type where
```
is accepted by GHC-9.4 with just `-XHaskell2010 -XGADTSyntax -XKindSignatures`. GHC-9.2 and older require `DataKinds`. I cannot find anything in release notes justifying this change.
If it's intentional, please amend release notes.
--------------------------
Here is a specification for what `-XDataKinds` allows, or doesn't. First, some definitions:
* A user-written type (i.e. part of the source text of a program) is in a **kind context** if it follows a "::" in:
* A standalone kind signature (e.g. `type T :: Nat -> Type`)
* A kind signature in a type (e.g. `forall (a :: Nat -> Type). blah`, `type F = G :: Nat -> Type`, etc.)
* A result kind signature in a type declaration (e.g. `data T a :: Nat -> Type where ...`, `type family Fam :: Nat -> Type`, etc.)
* All other contexts where types can appear are referred to as **type contexts**.
* The **kind type constructors** are (see `GHC.Core.TyCon.isKindTyCon`):
* `TYPE` and `Type`
* `CONSTRAINT` and `Constraint`
* `LiftedRep`
* `RuntimeRep`, `Levity`, and their data constructors
* `Multiplicity` and its data construtors
* `VecCount`, `VecElem`, and their data constructors
* A **`type data` type constructor** is defined using the `TypeData` extension, such as the `T` in `type data T = A | B`.
* The following are rejected in type contexts unless `-XDataKinds` is enabled:
* Promoted data constructors (e.g., `'Just`), except for those data constructors listed under "kind type constructors"
* Promoted list or tuple syntax (e.g., `'[Int, Bool]` or `'(Int, Bool)`)
* Type-level literals (e.g., `42`, `"hello"`, or `'a'` at the type level)
* The following are rejected in kind contexts unless `-XDataKinds` is enabled:
* Everything that is rejected in a type context.
* Any type constructor that is not a kind type constructor or a `type data` type constructor (e.g., `Maybe`, `[]`, `Char`, `Nat`, `Symbol`, etc.)
Note that this includes rejecting occurrences of non-kind type construtors in type synomym (or type family) applications, even it the expansion would be legal. For example:
```hs
type T a = Type
f :: forall (x :: T Int). blah
```
Here the `Int` in `T Int` is rejected even though the expansion is just `Type`. This is consistent with, for example, rejecting `T (forall a. a->a)` without `-XImpredicativeTypes`.
This check only occurs in kind contexts. It is always permissible to mention type synonyms in a type context without enabling `-XDataKinds`, even if the type synonym expands to something that would otherwise require `-XDataKinds`.https://gitlab.haskell.org/ghc/ghc/-/issues/22139TypeError's interaction with type family injectivity2022-09-02T20:55:29ZGergő ÉrdiTypeError's interaction with type family injectivityLet's say I have the following Haskell code, using `TypeFamilyDependencies`:
```haskell
data FieldK
data Field (f :: FieldK)
type family FieldToFieldKList (fs :: [Type]) = (r :: [FieldK]) | r -> fs where
FieldToFieldKList '[] = '[]...Let's say I have the following Haskell code, using `TypeFamilyDependencies`:
```haskell
data FieldK
data Field (f :: FieldK)
type family FieldToFieldKList (fs :: [Type]) = (r :: [FieldK]) | r -> fs where
FieldToFieldKList '[] = '[]
FieldToFieldKList (Field f : fs) = f : FieldToFieldKList fs
FieldToFieldKList (a : fs) = TypeError (Text "Must be a Field: " :<>: ShowType a)
```
This is currently thrice rejected by GHC:
* `TypeError` is a type family, and injective type family equations cannot have type family applications on their right-hand side (*Verifying injectivity annotation* note, check 3)
* Type variables `a` and `fs` of `a : fs` cannot be inferred from the right-hand side `TypeError ...`. (check 4)
* Overlap between the right-hand sides `[]` and `TypeError ...`, because type family applications pre-unify with everything (check B2)
Without the third (the `TypeError`) clause, GHC accepts this type family definition as injective.
My question is whether these three rejection reasons can be alleviated by the fact that the RHS in question is a `TypeError`. The idea being, if somewhere inside a type we arrive at a `TypeError _`, this will lead to a type error anyway, so we won't try to solve any further type equations. So it shouldn't cause any problems if we could derive inconsistent equations from type family applications that reduce to `TypeError _`.https://gitlab.haskell.org/ghc/ghc/-/issues/22135Type family injectivity annotation is rejected with type variable rhs, even o...2022-09-08T12:32:47ZGergő ÉrdiType family injectivity annotation is rejected with type variable rhs, even on non-endomorphismIn [*Injective Type Families for Haskell*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf), the following explanation is given for rejecting bare type variables on RHS:
> ```
> type ...In [*Injective Type Families for Haskell*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/injective-type-families-acm.pdf), the following explanation is given for rejecting bare type variables on RHS:
> ```
> type family W1 a = r | r -> a
> type instance W1 [a] = a
> ```
>
> To a mathematician this function certainly looks injective. But,
> surprisingly, it does not satisfy Definition 1! Here is a counterexample. Clearly we do have a proof of `(W1 [W1 Int ] ∼
> W1 Int)`, simply by instantiating the type instance with `[a |-> W1 Int]`. But if `W1` was injective in the sense of Definition 1, we could derive a proof of `[W1 Int ] ∼ Int`, and that is plainly false!
>
> Similarly:
>
> ```
> type family W2 a = r | r -> a
> type instance W2 [a] = W2 a
> ```
>
> Again `W2` looks injective. But we can prove `W2 [Int] ∼ W2 Int`,
> simply by instantiating the type instance; then by Definition 1, we
> could then conclude `[Int] ∼ Int`, which is plainly false. So neither
> `W1` nor `W2` are injective, according to our definition. Note that the
> partiality of `W1` and `W2` is critical for the failure case to occur.
In addition to exploiting partiality, the first example also requires `W1` to be an endomorphism, and the second one depends on `[]` being an endomorphism.
So why is the following example still rejected, where the type family is not an endomorphism and not recursive; in fact, even total?
```
newtype Wrapper = Wrap Type
type family Unwrap (x :: Wrapper) = (r :: Type) | r -> x where
Unwrap (Wrap a) = a
```https://gitlab.haskell.org/ghc/ghc/-/issues/22127decomposeRuleLhs reports bogus error2022-09-03T21:05:00ZSimon Peyton JonesdecomposeRuleLhs reports bogus errorConsider
```
f :: Int -> Int
f x = x
{-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
```
Currently compiling with -O gives
```
Foo.hs:8:11: error:
Rule "foo": Forall'd variable ‘a’ does not appear on left hand side
...Consider
```
f :: Int -> Int
f x = x
{-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
```
Currently compiling with -O gives
```
Foo.hs:8:11: error:
Rule "foo": Forall'd variable ‘a’ does not appear on left hand side
|
8 | {-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
## Diagnosis
`GHC.HsToCore.Binds.decomposeRuleLhs` takes the free vars of the LHS and checks that all of those free vars are among the binders. But the (shallow) free vars of `f (g x)` are are just `{f,g,x}`, but not `a`. Yet `a` is a binder.
Clearly we want the *deep* free vars of the LHS for this error check.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/22101Redundant constraint warning does not account for pattern checking2022-09-23T21:47:18ZDavid FeuerRedundant constraint warning does not account for pattern checking## Summary
Constraints that are only required for pattern checking are falsely reported as redundant.
## Steps to reproduce
```haskell
{-# language DataKinds, GADTs, TypeOperators, AllowAmbiguousTypes #-}
{-# options_ghc -Wall -Wredun...## Summary
Constraints that are only required for pattern checking are falsely reported as redundant.
## Steps to reproduce
```haskell
{-# language DataKinds, GADTs, TypeOperators, AllowAmbiguousTypes #-}
{-# options_ghc -Wall -Wredundant-constraints #-}
import Data.Type.Bool
import Data.Type.Equality
-- | Singletons for 'Bool'
data SBool b where
SFalse :: SBool 'False
STrue :: SBool 'True
-- | If a disjunction is false, so is its left argument.
orL :: (a || b) ~ 'False => SBool a -> a :~: 'False
orL SFalse = Refl
```
GHC tells me the `(a || b) ~ 'False` constraint is redundant.
## Expected behavior
I expect the above to compile without warnings.
## Discussion
The constraint is redundant—for type checking: `orR` will pass the type checker if it's removed. However, it's *not* redundant for pattern checking—the pattern checker will produce a warning if it's removed. Is there a way to account for which constraints the pattern checker "uses", and avoid warning about ones that it does?
## Environment
* GHC version used: 9.4.1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/22079Free variable finders are confused about coercion holes2022-08-30T22:17:45ZRichard Eisenbergrae@richarde.devFree variable finders are confused about coercion holes**Definition.** A *deep* traversal to collect free variables means that the traversal collects also the free variables in the kinds of free variables. These are also sometimes called the deep free variables.
When collecting free variabl...**Definition.** A *deep* traversal to collect free variables means that the traversal collects also the free variables in the kinds of free variables. These are also sometimes called the deep free variables.
When collecting free variables deeply of a type, GHC does a strange thing when recurring into the kinds of the variables: it zaps the set of in-scope variables, as documented in Note [Closing over free variable kinds] in GHC.Core.TyCo.Rep (and summarized in this para). For example, if we are collecting the free variables of `forall a b. a -> b -> Proxy c`, we do not want to return `a` and `b` as free variables. We thus remember these as locally in scope, so that we skip occurrences. However, we do *not* want to retain `a` and `b` as in scope when traversing the kind of `c`. Why not? Let's imagine `c :: Either a b`, so that we have `forall a b. a -> b -> Proxy (c :: Either a b)`. Now, are `a` and `b` free? Yes! That's because `c` is not locally bound -- it must have come into scope previously. Accordingly, the `a` and `b` in its kind are *not* the `a` and `b` bound by that `forall` we're all looking at -- they also must be bound further up. The simple solution is to drop the in-scope set when traversing a free variable kind. This is implemented today.
The problem is for coercion holes. (The problem presumably *also* happens for metavariables, but it came up in the context of coercion holes.) Specifically, look at this function:
```hs
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoFVsOfImplic :: Implication -> FV
-- Only called on *zonked* things
tyCoFVsOfImplic (Implic { ic_skols = skols
, ic_given = givens
, ic_wanted = wanted })
| isEmptyWC wanted
= emptyFV
| otherwise
= tyCoFVsVarBndrs skols $
tyCoFVsVarBndrs givens $
tyCoFVsOfWC wanted
```
In the main body of this function, we bind the skolems and the givens and then traverse (deeply) the wanteds. The fact that we bind the skolems and the givens means that skolems and givens will *not* be considered free (good). But now consider this:
```
forall a. [W] hole_abc :: a ~ Bool
[W] hole_def :: ... |> hole_abc ...
```
When traversing the type of `hole_abc`, we see that the `a` is a skolem and refuse to add it to the fv set. Good. But when traversing the type of `hole_def`, we see an *occurrence* of `hole_abc` and then look in its type *without an in-scope set*. So we report `a` as free! Disaster!
The root problem here is that coercion holes (resp. metavariables) aren't really bound. They *are* local to a certain TcLevel, which could in theory be used to know whether to consider them "bound-like" or "free-like" (i.e. the level could be used to set whether to zap the in-scope set when traversing an occurrence's kind), but that would add considerable complication to free-variable finding.
There is not, as far as I know, a live bug around this issue. That's because the implementation doesn't meet the specification, as we can see in this code:
```hs
tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
= tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
tyCoFVsOfCoVar v fv_cand in_scope acc
= (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
```
Note that the `in_scope` set is *not* zapped when recurring in `varType v`. So, despite the logic at the top of this post, we don't actually apply it in `tyCoFVsOfCoVar`. (We do apply it in lots of other places.) Interestingly, the lack of zapping affects ordinary covars, not just coercion holes, and so is quite possibly a bug-in-waiting. (We just don't have enough locally bound covars to notice.)
My Tweag intern @yiyunliu is revamping free-variable finders. In his new version, he fixed the bug, but then that caused the "Disaster!" described above. (If it's helpful, I imagine he can provide more concrete details.)
I think the right answer here is to add the zapping logic to the recurrence into covar kinds, but then also to add logic to `tyCoFVsOfImplic` to consider the coercion holes bound when traversing the types of the wanteds in a WC. Then, the free-var finder won't traverse the holes' kinds at all, avoiding the problem described here.
This whole area still makes me nervous though: given that a coercion hole (resp. metavariable) stands for an as-yet-unknown coercion (resp. type), taking the free variables of any type that has holes (metavars) seems dodgy, even though it's quite useful.https://gitlab.haskell.org/ghc/ghc/-/issues/22065Core Lint error from PartialTypeSignatures2022-08-18T20:59:40ZIcelandjackCore Lint error from PartialTypeSignaturesRunning on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f ...Running on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f :: [_] -> Int
f = length @[] @_
x :: [_]
x = mempty @[_]
```
```
ghci> :load ~/hs/5613.hs
[1 of 1] Compiling Main ( /home/baldur/hs/5613.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
/home/baldur/hs/5613.hs:8:20: warning:
The type variable @k_a9Dn[sk:1] is out of scope
In the RHS of foo :: Foo
In the body of letrec with binders x_a9sr :: forall {w}. [w]
In the body of letrec with binders f_a9sq :: forall {w}. [w] -> Int
In the body of lambda with binder a_a9Dz :: k_a9Dn[sk:1]
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$tcFoo :: TyCon
[LclIdX]
$tcFoo
= TyCon
13795410111426859749##
2910294326838708211##
$trModule
(TrNameS "Foo"#)
0#
krep$*
$tc'Apply :: TyCon
[LclIdX]
$tc'Apply
= TyCon
16548517680761376676##
14341609333725595319##
$trModule
(TrNameS "'Apply"#)
1#
$krep_a9DG
$krep_a9DI [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DI = $WKindRepVar (I# 0#)
$krep_a9DH [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DH = KindRepFun $krep_a9DI $krep_a9DJ
$krep_a9DK [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DK = KindRepFun $krep_a9DI $krep_a9DL
$krep_a9DG [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DG = KindRepFun $krep_a9DH $krep_a9DK
$krep_a9DJ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DJ = KindRepTyConApp $tcInt ([] @KindRep)
$krep_a9DL [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DL = KindRepTyConApp $tcFoo ([] @KindRep)
$trModule :: Module
[LclIdX]
$trModule
= Module (TrNameS "plutarch-core-0.1.0-inplace"#) (TrNameS "Main"#)
foo :: Foo
[LclIdX]
foo
= letrec {
x_a9sr :: forall {w}. [w]
[LclId]
x_a9sr
= \ (@w_a9CP) ->
let {
$dMonoid_a9CV :: Monoid [w_a9CP]
[LclId]
$dMonoid_a9CV = $fMonoid[] @w_a9CP } in
letrec {
x_a9CR :: [w_a9CP]
[LclId]
x_a9CR = break<0>() mempty @[w_a9CP] $dMonoid_a9CV; } in
x_a9CR; } in
letrec {
f_a9sq :: forall {w}. [w] -> Int
[LclId]
f_a9sq
= \ (@w_a9D6) ->
let {
$dFoldable_a9De :: Foldable []
[LclId]
$dFoldable_a9De = $fFoldable[] } in
letrec {
f_a9D8 :: [w_a9D6] -> Int
[LclId]
f_a9D8 = break<1>() length @[] $dFoldable_a9De @w_a9D6; } in
f_a9D8; } in
break<2>(x_a9sr,f_a9sq)
(\ (@(a_a9Dz :: k_a9Dn[sk:1])) ->
(\ (@k_a9Dn) (@(a_a9Do :: k_a9Dn)) ->
(\ (@x_X0) (ds_d9DO :: x_X0 -> Int) (ds_d9DP :: x_X0) ->
Apply @x_X0 ds_d9DO ds_d9DP)
@[Any @Type] (f_a9sq @(Any @Type)) (x_a9sr @(Any @Type)))
@(Any @Type) @(Any @(Any @Type)))
@(Any @k_a9Dn[sk:1])
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
ghci>
```https://gitlab.haskell.org/ghc/ghc/-/issues/22063Forall-types should be of a TYPE kind2023-12-04T13:51:21ZmniipForall-types should be of a TYPE kindThis is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`...This is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`-quantified type to be inhabited by values, i.e. that `forall a. {- ... -} :: TYPE r` for some `r`. Apparently this is never checked in GHC and we have roughly:
```
Gamma, a |- t :: k
---------------------------
Gamma |- (forall a. t) :: k
```
This implies that all kinds (even closed) are lifted: `forall a. a :: k`. Of course in presence of TypeFamilies+UndecidableInstances all kinds are already lifted, but this seems somehow worse.
Furthermore such a type can be used to trigger a core lint error, the wording of which ("Non-*-like kind when *-like expected") suggests that at least on some level it is expected that `forall a. ... :: *`. Applying a type constructor (other than `->`) to a type like `forall a. a` requires ImpredicativeTypes, but (and this might be an unrelated issue) apparently the type can appear on the left side of an application even without ImpredicativeTypes.
## Steps to reproduce
GHCi says:
```hs
> :kind forall a. a
forall a. a :: k
```
The following are accepted by GHC 9.2.3, 8.6.5 and HEAD:
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures #-}
module M where
type F = (forall (f :: * -> *). f) ()
f :: F
f = f
```
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, ImpredicativeTypes #-}
module M where
type B = forall (a :: Bool). a
b :: proxy B
b = b
```
but with `-dcore-lint` they explode:
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
a.hs:5:1: warning:
Non-Type-like kind when Type-like expected: * -> *
when checking the body of forall: f_agw
In the type of a binder: f
In the type ‘F’
Substitution: [TCvSubst
In scope: InScope {f_agw}
Type env: [agw :-> f_agw]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
f :: F
[LclIdX]
f = f
end Rec }
*** End of Offense ***
```
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
b.hs:5:1: warning:
Non-Type-like kind when Type-like expected: Bool
when checking the body of forall: a_auh
In the type of a binder: b
In the type ‘forall (proxy :: Bool -> *). proxy B’
Substitution: [TCvSubst
In scope: InScope {a_auh proxy_aui}
Type env: [auh :-> a_auh, aui :-> proxy_aui]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
b :: forall (proxy :: Bool -> *). proxy B
[LclIdX]
b = \ (@(proxy_awC :: Bool -> *)) -> b @proxy_awC
end Rec }
*** End of Offense ***
```
GHC 8.4.4 will fail the first program with an impredicativity error, but will still accept it with ImpredicativeTypes enabled, and will still crash with a core lint.
## Expected behavior
`forall a. e` should constrain `e :: TYPE r`, meaning GHCi should report `forall a. a :: *` or `forall a. a :: TYPE r`. Both programs should be rejected with a type error for the above reason. The first program (or programs like it) should raise an "Illegal impredicative type".
## Environment
* GHC version used: 8.4.4, 8.6.5, 9.2.3, HEAD
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21995-Wunused-type-patterns warns on used type variables2023-05-26T07:36:09ZLas Safin-Wunused-type-patterns warns on used type variables## Summary
```haskell
import Data.Kind (Type)
type family UnApply (fx :: Type) :: Type -> Type where
forall (f :: Type -> Type) (x :: Type).
UnApply (f x) = f -- warns about unused `x`
```
```
[1 of 1] Compiling Main ...## Summary
```haskell
import Data.Kind (Type)
type family UnApply (fx :: Type) :: Type -> Type where
forall (f :: Type -> Type) (x :: Type).
UnApply (f x) = f -- warns about unused `x`
```
```
[1 of 1] Compiling Main ( Test.hs, interpreted )
Test.hs:4:31: warning: [-Wunused-type-patterns]
Defined but not used on the right hand side: type variable ‘x’
|
4 | forall (f :: Type -> Type) (x :: Type).
| ^
```
If a type variable is *needed* on the LHS, yet not used on the RHS,
GHC will warn with -Wunused-type-patterns, even if removing that variable or
replacing it with `_` will give an error.
## Steps to reproduce
Compile above example with `-Wunused-type-patterns`.
## Expected behavior
It should not give a warning.
## Environment
* GHC version used: 9.2.4sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21935Implementation of GHC.TypeLits.<= is still not quite right2023-03-21T15:21:25ZChristiaan BaaijImplementation of GHC.TypeLits.<= is still not quite right`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC ...`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC 7.8) we got:
```haskell
type x <= y = (x <=? y) ~ True
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
Where only `<=?` had hard-coded resolution rules.
And for a very long time all was right with the world.
Then, in `base-4.16` (GHC 9.2) we suddenly got:
```haskell
type x <= y = (x <=? y) ~ True
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
type OrdCond :: Ordering -> k -> k -> k -> k
type family OrdCond o lt eq gt where
OrdCond 'LT lt eq gt = lt
OrdCond 'EQ lt eq gt = eq
OrdCond 'GT lt eq gt = gt
type Compare :: k -> k -> Ordering
type family Compare a b
type instance Compare (a :: Natural) b = CmpNat a b
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
```
Where only `CmpNat` has hard-coded resolution rules.
This new implementation of `<=` had error messages of much porer quality than previous implementations, which was reported in #20009.
For the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where
import Data.Proxy
import GHC.TypeLits
proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()
proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```
we went from this error message in GHC 9.0:
```
$ ghci TestInEq.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
```
to this error message in GHC 9.2:
```
$ ghci TestInEq.hs
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘Data.Type.Ord.OrdCond
(CmpNat a (a + 1)) 'True 'True 'False’
with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
```
The quality of the error message was fixed in !6066, which is currently included to be part of the GHC 9.4.1 release.
In !6066 the implementation of `<=` was changed to:
```haskell
type x <= y = Assert (x <=? y) (LeErrMsg x y)
type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
```
which would create error messages of the following shape instead:
```
• Cannot satisfy: a <= a + 1
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
```
## Remaining issue
The problem with the !6066 implementation is that the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies #-}
module KnownNat2 where
import GHC.TypeLits
class KnownNat2 (name :: Symbol) (a :: Nat) (b :: Nat) where {}
instance (b <= a) => KnownNat2 "-" a b
```
that used to compile without errors, now gives the following error (this is with the GHC 9.4.1-rc1 release):
```
GHCi, version 9.4.0.20220721: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling KnownNat2 ( KnownNat2.hs, interpreted )
KnownNat2.hs:9:10: error:
* Variables `b, a' occur more often
in the constraint `b <= a'
than in the instance head `KnownNat2 "-" a b'
(Use UndecidableInstances to permit this)
* In the instance declaration for `KnownNat2 "-" a b'
|
9 | instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 "-" a b
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
```https://gitlab.haskell.org/ghc/ghc/-/issues/21909UndecidableSuperClasses fails to terminate when inferring type in where-clause2023-03-09T14:52:54ZBrandon ChinnUndecidableSuperClasses fails to terminate when inferring type in where-clause## Summary
When defining a class with a recursive constraint on an associated type family, functions using that constraint fail to type check when inferring type in a where clause.
Related to:
* https://gitlab.haskell.org/ghc/ghc/-/iss...## Summary
When defining a class with a recursive constraint on an associated type family, functions using that constraint fail to type check when inferring type in a where clause.
Related to:
* https://gitlab.haskell.org/ghc/ghc/-/issues/20836
* https://gitlab.haskell.org/ghc/ghc/-/issues/19627
## Steps to reproduce
The following fails on all GHC versions I've tested, 8.2 to 9.4.1-rc1.
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableSuperClasses #-}
import Data.Kind
class (Monad m, MyMonad (Inner m)) => MyMonad m where
type Inner m :: Type -> Type
foo :: m Int
works :: MyMonad m => m String
works = show <$> ((+ 1) <$> foo)
fails :: MyMonad m => m String
fails = show <$> fooPlusOne
where
fooPlusOne = (+ 1) <$> foo
alsoFails :: MyMonad m => m String
alsoFails =
let fooPlusOne = (+ 1) <$> foo
in show <$> fooPlusOne
```
This errors with:
```
• solveWanteds: too many iterations (limit = 4)
Unsolved: WC {wc_simple =
[D] _ {0}:: Monad f0 (CDictCan)
[D] _ {0}:: Monad (Inner f0) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: Applicative f0 (CDictCan)
[D] _ {0}:: Applicative (Inner f0) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dFunctor_aJ3 {0}:: Functor f0 (CDictCan)
[D] _ {0}:: Functor (Inner f0) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dMyMonad_aJM {0}:: MyMonad f0 (CDictCan)
[D] _ {0}:: MyMonad (Inner f0) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: MyMonad
(Inner (Inner (Inner (Inner f0)))) (CDictCan(psc))}
Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
```
At least GHC 9.4.1-rc1 gives a slightly better error message in addition to `too many iterations`:
```
• Could not deduce (Monad
(Inner (Inner (Inner (Inner (Inner m))))))
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner (Inner m)))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner m))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner m)))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner m))’,
arising from a superclass required to satisfy ‘MyMonad (Inner m)’,
arising from a superclass required to satisfy ‘MyMonad m’,
arising from a use of ‘foo’
```
## Expected behavior
I know `-XUndecidableSuperClasses` always carries a risk of non-termination. Is this one of those cases that's known to just not work? Or should we try to make this work?
At the very least, I don't see any other issues around this simple example of just moving a thing into a where clause, so this at least provides a locus for discussion. It's also workaround-able by explicitly typing the helper function.
## Environment
* GHC version used: tested all GHC versions from 8.2 to 9.4.1-rc1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/21906FixedRuntimeRep: check type arguments instead of value arguments for Ids with...2023-07-18T12:23:35Zsheafsam.derbyshire@gmail.comFixedRuntimeRep: check type arguments instead of value arguments for Ids with no bindingCurrently, we rule out bad representation-polymorphism in primops (and other `Id`s with no binding) through `tcRemainingValArgs`, which checks that the remaining value arguments all have a fixed `RuntimeRep`.
However, @bgamari points ou...Currently, we rule out bad representation-polymorphism in primops (and other `Id`s with no binding) through `tcRemainingValArgs`, which checks that the remaining value arguments all have a fixed `RuntimeRep`.
However, @bgamari points out in #21868 that we also need to rule out representation-polymorphism in other places that aren't arguments, such as the return `RuntimeRep` `r_rep` of `catch#` or `keepAlive#`:
```haskell
catch# :: forall (r_rep :: RuntimeRep) (r :: TYPE r_rep) w.
(State# RealWorld -> (# State# RealWorld, r #) )
-> (w -> State# RealWorld -> (# State# RealWorld, r #) )
-> State# RealWorld
-> (# State# RealWorld, r #)
keepAlive# :: forall (a_lev :: Levity) (a :: TYPE (BoxedRep lev))
(r_rep :: RuntimeRep) (r :: TYPE r_rep).
a -> State# RealWorld -> (State# RealWorld -> r) -> r
```
Furthermore, it is not enough to rule out representation-polymorphism: #21868 points out that the current implementation of these primops imposes further restrictions on the representation, because the passing of evaluation results may happen via the stack (e.g. in the case of an unregisterised compiler). The current implementation allows non-`Void` `PrimRep`s that are word-sized or smaller. This means that `BoxedRep Lifted`, `BoxedRep Unlifted`, `WordRep`, `Word8Rep`, `AddrRep` for example are all OK, while `FloatRep`, `TupleRep '[]` and `TupleRep '[ IntRep, WordRep ]` are all disallowed. This is a detail of the current implementation of these primops; this limitation could conceivably be lifted (see discussion on #21868).
## Plan
Here's a plan, elaborated with @simonpj and @monoidal:
### Step 1: store concreteness information in `IdDetails`
`Id`s whose type quantifies over `RuntimeRep`s which must be instantiated to concrete `RuntimeRep`s should store this information in their `IdDetails`:
1. For primops, we can replace the "is rep-poly" `Bool` stored in the `PrimOpId` constructor with a collection of type variables and associated `ConcreteTvOrigin`. For example, `catch#` would say that the `RuntimeRep` variable needs to be instantiated to a concrete `RuntimeRep`.
2. For wired-in `Id`s with a compulsory unfolding and representation-polymorphic arguments, add a new constructor to `IdDetails` with this same information.
3. For unboxed tuples and sums, we know ahead of time that the `RuntimeRep` arguments should be concrete (the first half of the type arguments).
4. This leaves representation-polymorphic newtype constructors, for which this strategy won't work because it might be some type other than one of the quantified type variables which is required to be concrete. See [§ The newtype question](#the-newtype-question) below.
### Step 2: create Concrete metavariables when instantiating
When instantiating an `Id` which contains this information, use concrete metavariables instead of `TauTv`s for the appropriately tagged variables.
To be specific, in `tcInstFun.go1`, when we split off some type variables using `tcSplitSomeForAllTyVars`, if `acc` is empty (i.e. we are instantiating at the top-level, not in a nested situation) and the function being applied is an `Id` with no binding, look up which variables must be concrete from the `Id` and pass that information on to `instantiateSigma`, saying to use `newConcreteTyVarX` instead of `newMetaTyVarX` for those variables.
Other than the wrinkle with representation-polymorphic unlifted newtypes, this would **allow us to remove `tcRemainingValArgs`**, as we will be ensuring concreteness right at the source, when the type variables are created. This means we will be able to accept
```haskell
type R :: RuntimeRep
type family R where { R = IntRep }
myId :: forall (a :: TYPE R). a -> a
myId = coerce
```
effectively implementing PHASE 2 of FixedRuntimeRep for primops without having to pay the onerous implementation cost of inserting the correct coercions when eta-expanding.
### Step 3: check concreteness in Core Lint
The above steps attempt to instantiate these "MustBeConcrete" type variables to concrete types. We want to check that this is indeed the case, and that further transformations don't break the invariant. So we should also add a check to Core Lint to ensure that in any application of an `Id` with no binding, the types it requires to be concrete are indeed concrete.
## The newtype question
In [Step 1](#step-1), (4), we alluded to the observation that storing which type variables must be concrete might not be sufficient for representation-polymorphic newtype constructors. For example:
```haskell
type R :: Type -> RuntimeRep
type family R a
type family T :: Type -> TYPE (R a)
type family T a
type N :: forall (a :: Type) -> TYPE (R a)
data N a = MkN (T a)
```
In this case, the type that needs to be concrete is `R a`, which is not a type variable.
### Option 1: store types instead of type variables
We could directly store which types must be concrete, instead of referring to type variables which must be concrete. Then, to adapt the plan from [Step 2](#step-2), in `instantiateSigma` we would:
1. create new meta type variables as usual,
2. apply the obtained substitution to the types that must be concrete,
3. ensure these substituted types are concrete.
Unfortunately it isn't clear what we would do with the evidence.
### Option 2: change the newtype wrapper
We could change the newtype wrapper for `MkN` to be something like:
```haskell
MkN :: forall {conc :: RuntimeRep}. forall (a :: TYPE) -> R a ~# conc => T a -> N a
```
That is, we add an extra inferred type variable which must be concrete, and add an equality predicate between that concrete type variable and the representation of the type stored inside the newtype. We can then make use of this coercion in the compulsory unfolding of `MkN`. (The type variable `conc` is inferred and comes first, so as to not intefere with visible type applications.)
This brings us back to the case of type variables, which we can handle as in [Step 2](#step-2).
It isn't clear how much extra work this would be, as now we have a newtype worker, one of whose arguments is a coercion. This seems OK, as we already allow e.g. a newtype with a stupid theta. I think it would mean adding an `eq_pred` to the `Haskell98` datacon declaration however, and I don't know what knock-on consequences that might have.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21898Problems disambiguating a record update with pattern synonyms2023-03-30T13:28:39Zsheafsam.derbyshire@gmail.comProblems disambiguating a record update with pattern synonymsThe parent of a pattern synonym record field is the pattern synonym itself, which I think makes sense (a pattern synonym behaves much like a data constructor). However, it seems that the following variant on #21443 causes GHC to trip ove...The parent of a pattern synonym record field is the pattern synonym itself, which I think makes sense (a pattern synonym behaves much like a data constructor). However, it seems that the following variant on #21443 causes GHC to trip over:
```haskell
{-# LANGUAGE DuplicateRecordFields, PatternSynonyms #-}
pattern P :: Int -> Int -> (Int, Int)
pattern P { proj_x, proj_y } = (proj_x, proj_y)
pattern Q1 :: Int -> Int
pattern Q1 { proj_x } = proj_x
pattern Q2 :: Int -> Int
pattern Q2 { proj_y } = proj_y
blah :: (Int, Int) -> (Int, Int)
blah p = p { proj_x = 0, proj_y = 1 }
```
```
error:
* GHC internal error: `T21443b.$sel:proj_x:P' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [auv :-> Identifier[p::(Int,
Int), NotLetBound],
rgF :-> Identifier[blah::(Int, Int)
-> (Int, Int), TopLevelLet {} True]]
* In the expression: p {proj_x = 0, proj_y = 1}
In an equation for `blah': blah p = p {proj_x = 0, proj_y = 1}
|
| blah p = p { proj_x = 0, proj_y = 1 }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21896Panic when checking type family dependency2022-07-26T07:49:55ZGergő ÉrdiPanic when checking type family dependency```
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies, PolyKinds #-}
module Bug where
data T = Foo | Bar
type family F (ns :: T) (ret :: k) = (r :: k) | r -> ret where
F Foo r = r
F...```
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies, PolyKinds #-}
module Bug where
data T = Foo | Bar
type family F (ns :: T) (ret :: k) = (r :: k) | r -> ret where
F Foo r = r
F Bar r = r
```
On a GHC as of e2f0094c315746ff15b8d9650cf318f81d8416d7, with sufficient sanity checks (i.e. compiled with `-DDEBUG`), this crashes with:
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20220719:
ASSERT failed!
in_scope InScope {r_a9 k_aJ}
tenv [a9 :-> r_a9, aa :-> r_a9, aJ :-> k_aJ]
cenv []
tys [k_aN, r_aa]
cos []
needInScope {k_aN}
Call stack:
CallStack (from HasCallStack):
assertPpr, called at compiler/GHC/Core/TyCo/Subst.hs:645:5 in ghc:GHC.Core.TyCo.Subst
checkValidSubst, called at compiler/GHC/Core/TyCo/Subst.hs:694:17 in ghc:GHC.Core.TyCo.Subst
substTys, called at compiler/GHC/Core/FamInstEnv.hs:568:25 in ghc:GHC.Core.FamInstEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```https://gitlab.haskell.org/ghc/ghc/-/issues/21806Example in ghc doc for SAKS doesn't work2022-07-29T11:00:01ZGeorgi LyubenovExample in ghc doc for SAKS doesn't workNot sure if this is a bug or a documentation issue, but an example from the [ghc docs on SAKS](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/poly_kinds.html#standalone-kind-signatures-and-declaration-headers) doesn'...Not sure if this is a bug or a documentation issue, but an example from the [ghc docs on SAKS](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/poly_kinds.html#standalone-kind-signatures-and-declaration-headers) doesn't compile:
```haskell
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Kind
type GProx4 :: k -> Type
data GProx4 :: w where MkGProx4 :: GProx4 a
```
```sh
[nix-shell:~]$ ghci --version
The Glorious Glasgow Haskell Compilation System, version 9.2.2
[nix-shell:~]$ ghci /tmp/asdf.hs
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/googleson78/.ghci
[1 of 1] Compiling Main ( /tmp/asdf.hs, interpreted )
/tmp/asdf.hs:10:1: error:
• Couldn't match expected kind ‘w’ with actual kind ‘k -> *’
• In the data type declaration for ‘GProx4’
|
10 | data GProx4 :: w where MkGProx4 :: GProx4 a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
>
```sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21793PolyKinds: kind information for variables bound in instance heads propagates ...2022-07-04T09:11:09ZMichael Peyton JonesPolyKinds: kind information for variables bound in instance heads propagates surprisingly badly## Summary
Here's a a reduction of a program I was writing.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GA...## Summary
Here's a a reduction of a program I was writing.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Repro where
import Data.Kind
data P = L | R
data T (a :: P) where
A :: T a
B :: T R
type TConstraint = forall a . T a -> Constraint
class (forall a . constr @a A) => ForAllA (constr :: TConstraint)
instance (forall a . constr @a A) => ForAllA constr
```
GHC says:
```
Repro.hs:18:22: error:
• Cannot apply function of kind ‘k0’
to visible kind argument ‘a’
• In the instance declaration for ‘ForAllA constr’
|
18 | instance (forall a . constr @a A) => ForAllA constr
```
i.e. it has inferred that `constr` in the instance declaration should have kind `k`. I already find this suprising: the class declaration states that for this class, `constr` always has the given kind, so I'd have expected that to propagate. Anyway, let's try and fix it.
1. Kind signature on the instance head
```haskell
instance (forall a . constr @a A) => ForAllA (constr :: TConstraint)
```
Same error.
2. Standalone kind signatures
```haskell
type ForAllA :: TConstraint -> Constraint
class (forall a . constr @a A) => ForAllA constr
instance (forall a . constr @a A) => ForAllA constr
```
Same error.
3. Explicit quantification in the instance head
```haskell
instance forall (constr :: MethodConstraint) . (forall a . constr @a A) => ForAllA constr
```
That finally works!
I'm not totally surprised that 2 doesn't work, but I *am* surprised that 1 doesn't work. That's usually how we constrain type variables in the absence of standalone kind signatures (which we can't write for instance declarations).
## Steps to reproduce
The file above should be independently compilable.
## Environment
* GHC version used: 9.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/21765`-Wredundant-constraints` false positives in class instance contexts2023-08-31T04:27:45Zyairchu`-Wredundant-constraints` false positives in class instance contexts## Summary
In the following example:
```Haskell
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
class Functor f => C f where c :: f Int
instance (Functor f, Applicative f) => C f where c = pure 42
```
Compiling in GHC 9.2.3...## Summary
In the following example:
```Haskell
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
class Functor f => C f where c :: f Int
instance (Functor f, Applicative f) => C f where c = pure 42
```
Compiling in GHC 9.2.3 using `-Wredundant-constraints` produces the following warning:
```Haskell
test.hs:5:10: warning: [-Wredundant-constraints]
• Redundant constraint: Functor f
• In the instance declaration for ‘C f’
|
5 | instance (Functor f, Applicative f) => C f where c = pure 42
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
While the constraint intuitively seems redundant, in the case of instance contexts it is in fact necessary, by design, as [described here](https://stackoverflow.com/a/72690345/40916)
## Expected behavior
As in previous GHC versions, like 9.0.2, no warning should be given in this case.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21719Type checking with PartialTypeSignatures is broken2022-08-17T10:21:48ZDanil BerestovType checking with PartialTypeSignatures is broken## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
impor...## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
import Control.Exception
data Foo = Foo
deriving (Show, Exception)
class CanThrow e
qux :: Monad m => (CanThrow Foo => m a) -> m a
qux _ = undefined
class Monad m => MonadCheckedThrow m where
throwChecked :: (Exception e, CanThrow e) => e -> m a
foo :: MonadCheckedThrow m => m Int
foo = do
qux do
_ <- baz
pure 5
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
```
error:
• Could not deduce (CanThrow Foo)
from the context: MonadCheckedThrow m
bound by the type signature for:
foo :: forall (m :: * -> *). MonadCheckedThrow m => m Int
at _
or from: MonadCheckedThrow m1
bound by the inferred type for ‘baz’:
forall (m1 :: * -> *) a. MonadCheckedThrow m1 => m1 a
at _
• When checking that the inferred type
baz :: forall (m :: * -> *) a.
(CanThrow Foo, MonadCheckedThrow m) =>
m a
is as general as its (partial) signature
baz :: forall (m :: * -> *) a. MonadCheckedThrow m => m a
In an equation for ‘foo’:
foo
= do qux
do _ <- baz
....
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
## Expected behavior
GHC must check `bar`'s type.
By the way the following code is checked:
```haskell
baz :: (c ~ CanThrow, c Foo, _) => _
baz = throwChecked Foo
-- and
baz :: (f ~ Foo, CanThrow f, _) => _
baz = throwChecked Foo
-- and even
baz :: _ => CanThrow Foo => _
baz = throwChecked Foo
```
## Environment
* GHC version used: 8.10.7Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21702Default type family instance in class can not refer to all class parameters2022-07-05T17:54:22ZLas SafinDefault type family instance in class can not refer to all class parameters## Motivation
```haskell
import Data.Kind (Type)
-- You'd also have `RelF a ~ b` as a constraint, albeit it's not relevant here.
class Rel (a :: Type) (b :: Type) | a -> b where
type RelF a :: Type
type RelF a = b
```
This should ...## Motivation
```haskell
import Data.Kind (Type)
-- You'd also have `RelF a ~ b` as a constraint, albeit it's not relevant here.
class Rel (a :: Type) (b :: Type) | a -> b where
type RelF a :: Type
type RelF a = b
```
This should work, but it complains that `b` on the last line is out of scope.
```
Example.hs:5:17: error: Not in scope: type variable ‘b’
|
5 | type RelF a = b
```
## Proposal
This should ideally work.
I'm willing to fix this myself, and would appreciate some pointers as to which file/directory in GHC this pertains to.