GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-10-14T08:52:11Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18704GHC could not deduce constraint from itself2021-10-14T08:52:11ZrybochodonezzarGHC could not deduce constraint from itself## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynon...## Summary
following code:
```haskell
{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #-}
module Lib where
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
data a ::: b = a ::: b
class Pair f where
type Left f :: a
type Right f :: b
instance Pair (a '::: b) where
type Left (a '::: b) = a
type Right (a '::: b) = b
class NC (x :: k)
instance NC (x :: k)
data L1 c f xs where
LC :: c x => f x -> L1 c f xs -> L1 c f (x ': xs)
LN :: L1 c f '[]
class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)
data f1 :*: f2 :: (kx ::: ky) -> * where
(:*:) :: f1 x -> f2 y -> (f1 :*: f2) (x '::: y)
pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) -> e
pairC e = e
type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s -> t a -> Foo t xs -> Foo t (s '::: a ': xs)
pattern Foo p t xs <- LC (p :*: t) xs where
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
```
Results in this compile error:
```
/home/ryba/ghc-bug/src/Lib.hs:38:46: error:
• Could not deduce (PairC KnownSymbol NC (s '::: a))
arising from a use of ‘LC’
from the context: KnownSymbol s
bound by the signature for pattern synonym ‘Foo’
at src/Lib.hs:(37,1)-(38,61)
or from: PairC KnownSymbol NC (s '::: a)
bound by a type expected by the context:
PairC KnownSymbol NC (s '::: a) =>
L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
at src/Lib.hs:38:45-61
• In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
In an equation for ‘Foo’:
Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
|
38 | Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
| ^^^^^^^^^^^^^^^
```
Which basically boils down to "could not deduce a from a"
## Environment
* GHC version used: 8.10.2
* stack resolver=nightly-2020-09-14
Optional:
* Operating System: Ubuntu
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/18645Incremental `tcCheckSatisfiability` API2021-07-26T09:54:10ZSebastian GrafIncremental `tcCheckSatisfiability` APIThe pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `...The pattern-match checker makes use of the function `tcCheckSatisfiability :: Bag EvVar -> TcM Bool` (henceforth `tcCS`) offered by the type-checker to solve type constraints. Over the course of a pattern-match checking session, such a `Bag EvVar` is accumulated and incrementally checked after each addition. As #17836 shows in a rather painful way, that scales quadratically, because the type-checker chews through the same type constraints over and over again.
But look at how the pattern-match checker uses `tcCS`:
```hs
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; let new_inert = inert `unionBags` evs
; ... <- initTcDsForSolver $ tcCheckSatisfiability new_inert
; ... }
```
The `inert` set is a `Bag EvVar` for which *we already know they are compatible with each other*, as they were checked by `tcCS` in a previous call. Only `cts :: Bag PredType` are unchecked. And as far as the pattern-match checker is concerned, the type of `inert` is completely opaque, so the API to `tcCS` could very well be
```hs
tcCheckSatisfiability :: TcInert -> Bag EvVar -> TcM (Maybe TcInert)
-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
; ...mb_new_inert... <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; ... }
```
I'm sure there already is something like `TcInert` in the type-checker. Looking at the implementation of `tcCS`, that might be the unused `EvBindMap`, but I'm not sure. Or is it the `InertCans` in `getInertCans`/`setInertCans`? CC @rae, @RyanGlScott, @simonpj
This blocks #17836 and would probably lead to quite a few (possibly rather drastic) metric decreases in other cases.https://gitlab.haskell.org/ghc/ghc/-/issues/18542Kind error when using partial type signatures2020-08-06T21:34:14Zlennart@augustsson.netKind error when using partial type signatures## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}...## Summary
When using a partial type signature I get a kind error, which is surprising.
## Steps to reproduce
Compile the following module. The function bar type checks, whereas baz gets a kind error
```
{-# LANGUAGE RankNTypes #-}
module Bug where
foo :: (Functor g) =>
(forall aa . Num aa => f aa -> g aa) ->
f a -> g (f a)
foo f x = undefined
bar :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> Int -> f a
bar f = foo f
baz :: (forall aa . Num aa => f aa -> Int -> aa) ->
f a -> _ -> f a
baz f = foo f
```
## Environment
* GHC version used:
The Glorious Glasgow Haskell Compilation System, version 8.10.19.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18481Improve instantiation of datacons2022-04-12T17:01:42ZKrzysztof GogolewskiImprove instantiation of dataconsThis ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic con...This ticket tracks a possible improvement to `return_data_con`.
When typechecking a datacon `T`, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.
Currently, we instantiate levity-polymorphic constructors. Quoting Note [Linear fields generalization]:
```
A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
certain newtypes with -XUnliftedNewtypes) then this strategy produces
\r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)
Which has type
forall r1 r2 a b. a #p-> b #q-> (# a, b #)
Which violates the levity-polymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.
So we really must instantiate r1 and r2 rather than quantify over them. For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
anywhere.
A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.
```
The goal of this ticket is to implement the last paragraph.https://gitlab.haskell.org/ghc/ghc/-/issues/18451Infinite loop during kind inference2020-07-27T08:10:18ZSimon Peyton JonesInfinite loop during kind inferenceThis program
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k -> k -> Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an ...This program
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type Const a b = a
data SameKind :: k -> k -> Type
type T (k :: Const Type a) = forall (b :: k). SameKind a b
```
goes into an infinite loop during kind checking. (Extracted from #16245.)
We have
```
a_agk :: k_au5
k_atM :: Const Type a_agk
k_au5 := k_au7
```
and then we try to unify `k_au7 := k_atM`. That should be an occurs-check error, since `k_atM`'s kind mentions `a_agk`, whose kind mentions `k_au5`, which is equal to `k_au7`.
But `occCheckExpand` (called from `GHC.Tc.Utils.Unify.metaTyVarUpdateOK`) expands the `Const` synonym in `k_atM`'s kind so that it no longer mentions `a_agk`, which allows the update to go ahead.
Wrong! We can't do this `occCheckExpand` business inside kinds! Let's just not do that.https://gitlab.haskell.org/ghc/ghc/-/issues/18439Pattern guards can break linearity2021-01-08T16:49:06ZArnaud SpiwackPattern guards can break linearity## Summary
Patterns, in pattern-guards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
...## Summary
Patterns, in pattern-guards guards are not checked for linearity. Which let's us write incorrect program with respect to linearity. The linter rightfully rejects those.
## Steps to reproduce
This typechecks but should not:
```
{-# LANGUAGE LinearTypes #-}
unsafeConsume :: a #-> ()
unsafeConsume x | _ <- x = ()
```
## Environment
* GHC version used: master 3656dff8259199d0dab2d1a1f1b887c252a9c1a3
## Note
Originally reported by Roman Cheplyaka.Arnaud SpiwackArnaud Spiwackhttps://gitlab.haskell.org/ghc/ghc/-/issues/18412Monotype check for case branches should not recur through arrows2020-07-20T07:57:36ZRichard Eisenbergrae@richarde.devMonotype check for case branches should not recur through arrowsConsider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted ...Consider this module:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
hr :: (forall a. a -> a) -> ()
hr _ = ()
foo x = case x of () -> hr
bar x = case x of True -> hr
False -> hr
```
On HEAD, `foo` is accepted while `bar` is rejected. (This is not a change from previous behavior.) The reason is that GHC requires `case` branches (when there are more than 1; and when the result of the `case` is being inferred, not checked) to have monotypes, lest it be left with the task of finding the most general supertype of a bunch of polytypes. However, now that we have simplified subsumption, it is draconian to propagate the monotype check past arrows. I thus claim that `bar` should be accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/18406Functional dependency should constrain local inferred type, but does not2022-02-23T13:21:42ZRichard Eisenbergrae@richarde.devFunctional dependency should constrain local inferred type, but does notIf I compile
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Bug where
class C a b | a -> b where
op :: a -> a
foo :: C a b => a -> b -> a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with...If I compile
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Bug where
class C a b | a -> b where
op :: a -> a
foo :: C a b => a -> b -> a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `-ddump-tc -fprint-typechecker-elaboration -fprint-explicit-foralls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a -> b -> a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT -> a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a -> a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.https://gitlab.haskell.org/ghc/ghc/-/issues/18311Record update is over-restrictive2022-05-26T07:40:34ZSimon Peyton JonesRecord update is over-restrictiveConsider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int -> T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int -> T Bool
foo2 t = t { y = True...Consider
```
type family F a
type instance F Int = Int
type instance F Bool = Int
data T a = MkT { x :: F a, y :: a }
foo1 :: T Int -> T Bool
foo1 (MkT { x = x }) = MkT { x = x, y = True}
foo2 :: T Int -> T Bool
foo2 t = t { y = True }
```
`foo1` typechecks fine, but `foo2` complains
```
Foo.hs:16:10: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: T Bool
Actual type: T Int
• In the expression: t {y = True}
In an equation for ‘foo2’: foo2 t = t {y = True}
```
This is bogus. `foo2` should be fine -- precisely because `foo1` is.
The offending code is in the `RecordUpd` case of `GHc.Tc.Gen.Expr.tcExpr`. See this comment
```
-- STEP 4 Note [Type of a record update]
-- Figure out types for the scrutinee and result
-- Both are of form (T a b c), with fresh type variables, but with
-- common variables where the scrutinee and result must have the same type
-- These are variables that appear in *any* arg of *any* of the
-- relevant constructors *except* in the updated fields
```
With the advent of type families "appearing in" a type is not the same as being fixed by it.
Not hard to fix; might even lead to less code!https://gitlab.haskell.org/ghc/ghc/-/issues/18300UnliftedNewtypesDifficultUnification broken due to simplified subsumption2020-07-03T21:33:23ZBen GamariUnliftedNewtypesDifficultUnification broken due to simplified subsumption`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`-enabled compiler.
```
Compile failed (exit code 1) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.202...`UnliftedNewtypesDifficultUnification` fails due to simplified subsumption patch (!2600) in `DEBUG`-enabled compiler.
```
Compile failed (exit code 1) errors were:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200603:
ASSERT failed! file compiler/GHC/Core/FamInstEnv.hs, line 651
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for UnliftedNewtypesDifficultUnification(normal)
```
I have marked this test as broken in the interest of getting !2600 merged.
As seen in Job [#356282](https://gitlab.haskell.org/ghc/ghc/-/jobs/356282).9.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/18151Eta-expansion of a left-section2021-01-12T23:04:49ZRichard Eisenbergrae@richarde.devEta-expansion of a left-sectionIf I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Exp...If I say
```hs
x = seq (True `undefined`) ()
```
what should I get when evaluating `x`?
According to my understanding of the Haskell Report, I should get `()`. And according to my understanding of GHC's source code (in `GHC.Tc.Gen.Expr`), I should get `()`. But I get an exception.
Why?
NB: `-XPostfixOperators` is off. If it were on, the exception would be expected.
Spun off from https://github.com/ghc-proposals/ghc-proposals/pull/275#issuecomment-6242820229.0.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/18073Out-of-date commentary in Tc.Deriv.Infer2020-04-23T03:49:06ZRichard Eisenbergrae@richarde.devOut-of-date commentary in Tc.Deriv.InferCheck out https://gitlab.haskell.org/ghc/ghc/-/blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addi...Check out https://gitlab.haskell.org/ghc/ghc/-/blob/15ab6cd548f284732a7f89d78c2b89b1bfc4ea1d/compiler/GHC/Tc/Deriv/Infer.hs#L805
* The commentary there talks about creating a variable `unsolved`, which does not seem to exist.
* In addition, the partition below creates `bad`, which is just ignored. Maybe this is right -- I have not thought about it. But if it is right, it should be documented.
cc @RyanGlScotthttps://gitlab.haskell.org/ghc/ghc/-/issues/17955mkNewTyConRhs panic when trying to constrain newtype with Coercible2021-01-23T06:44:33ZmatzemathicsmkNewTyConRhs panic when trying to constrain newtype with Coercible## Summary
The following code panics in ghc 8.8.3:
```haskell
{-# LANGUAGE FlexibleContexts #-}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
gh...## Summary
The following code panics in ghc 8.8.3:
```haskell
{-# LANGUAGE FlexibleContexts #-}
import Data.Coerce
newtype T = Coercible () T => T ()
```
Error message:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.3 for x86_64-unknown-linux):
mkNewTyConRhs
T [Coercible () T, ()]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/BuildTyCl.hs:65:27 in ghc:BuildTyCl
```
This seems to come from whatever is done to infer Coercible's instances.
Any other Constraint (weather or not using a multi parameter class) gives an error message:
```haskell
{-# LANGUAGE FlexibleContexts #-}
newtype T = Show T => T ()
```
results in:
```
[1 of 1] Compiling Main ( abug.hs, abug.o )
abug.hs:3:13: error:
* A newtype constructor cannot have a context in its type
T :: Show T => () -> T
* In the definition of data constructor `T'
In the newtype declaration for `T'
|
3 | newtype T = Show T => T ()
| ^^^^^^^^^^^^^^
```
## Expected behavior
Should most likely print an error message as in the second example.
## Environment
* GHC version used: 8.8.39.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/17873Lazy instantiation is incompatible with implicit parameters2020-07-15T09:06:16ZRichard Eisenbergrae@richarde.devLazy instantiation is incompatible with implicit parametersIn thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool -> Bool) => Bool -> Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: ...In thinking about issues around #17173, I came up with this silliness:
```hs
getx :: (?x :: Bool -> Bool) => Bool -> Bool
getx = ?x
z3 = (let ?x = not in getx) False
```
GHC's current response is utter garbage:
```
Scratch.hs:52:23: error:
• Couldn't match type ‘?x::Bool -> Bool’ with ‘Bool’
Expected type: Bool -> Bool -> Bool
Actual type: (?x::Bool -> Bool) => Bool -> Bool
• In the expression: getx
In the expression: let ?x = not in getx
In the expression: (let ?x = not in getx) False
|
52 | z3 = (let ?x = not in getx) False
|
```
The "couldn't match type" bit is ill-kinded, and I have no idea why GHC is expecting `Bool -> Bool -> Bool` here. But the root cause, I believe, is lazy instantiation. Functions are instantiated lazily. So the `let ?x = not in getx` is instantiated lazily. The body of a `let` inherits its instantiation behavior from the outer context. So the `getx` is instantiated lazily. This means that GHC happily infers type `(?x :: Bool -> Bool) => Bool -> Bool` for `getx`. And then, with no incentive to instantiate, it infers `(let ?x = not in getx) :: (?x :: Bool -> Bool) => Bool -> Bool`. Now, when we apply such a thing to a term argument, GHC instantiates. But, lo!, there is no longer a `?x :: Bool -> Bool` constraint in scope, causing unhappiness.
If we instantiate eagerly, I claim this should all work just fine.
I believe this will be fixed alongside #17173, but given that #17173 is about general improvement rather than bug-fixing, I made this outright bug a separate ticket.https://gitlab.haskell.org/ghc/ghc/-/issues/17841"No skolem info" panic with PolyKinds2020-10-19T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy...## Summary
Making a class with a kind-polymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{-# LANGUAGE PolyKinds #-}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)
|
5 | class Foo (t :: k) where foo :: Proxy (a :: t)
|
```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/17827Deduplicate overlapping Notes [TyVar/TyVar orientation] in TcUnify and [Canon...2020-02-14T16:54:11ZRichard Eisenbergrae@richarde.devDeduplicate overlapping Notes [TyVar/TyVar orientation] in TcUnify and [Canonical orientation for tyvar/tyvar equality constraints] in TcCanonicalThese Notes cover similar ground but say different things.These Notes cover similar ground but say different things.https://gitlab.haskell.org/ghc/ghc/-/issues/17789Instantiation doesn't look through dictionaries2020-02-05T11:16:36ZRichard Eisenbergrae@richarde.devInstantiation doesn't look through dictionariesThe bug is simple to state in terms of GHC's implementation: `topInstantiate` does not look past dictionaries. Thus a type like `forall a. C a => forall b. ...` only gets its `a` instantiated, not its `b`. This can be witnessed is some u...The bug is simple to state in terms of GHC's implementation: `topInstantiate` does not look past dictionaries. Thus a type like `forall a. C a => forall b. ...` only gets its `a` instantiated, not its `b`. This can be witnessed is some ugly-looking code:
```hs
data Rec a b = MkRec { x :: Bool }
class C a where
r :: Rec a b
instance C Int where
r = MkRec { x = True }
foo :: Rec Int Bool
foo = r { x = False }
```
This fails with
```
/Users/rae/temp/Bug.hs:10:7: error:
• Ambiguous type variable ‘a0’ arising from a use of ‘r’
prevents the constraint ‘(C a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instance exist:
instance C Int -- Defined at /Users/rae/temp/Bug.hs:6:10
• In the expression: r
In the expression: r {x = False}
In an equation for ‘foo’: foo = r {x = False}
```
I have no idea why it's an ambiguous-variable error, but let's not get distracted by that. The problem is that GHC does not instantiate `r` vigorously enough to notice that it's a record. The solution is straightforward: have `topInstantiate` be recursive, looking past dictionaries. `topInstantiate` is used in other places, too, and perhaps there are other similar bugs to find.https://gitlab.haskell.org/ghc/ghc/-/issues/17772CUSK-less class typechecks on 8.4, but not on 8.6+2021-03-31T17:39:10ZRyan ScottCUSK-less class typechecks on 8.4, but not on 8.6+This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (...This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x -> T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x -> T x
In the class declaration for ‘C’
|
13 | Proxy x -> T x
| ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k -> Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x -> T x
```https://gitlab.haskell.org/ghc/ghc/-/issues/17710Poly-kinded rewrite rule fails to typecheck (HEAD only)2020-03-15T18:51:16ZRyan ScottPoly-kinded rewrite rule fails to typecheck (HEAD only)I originally noticed this issue since it prevents the `free-algebras-0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage/-/jobs/240129)). Here is a minimized example that demonst...I originally noticed this issue since it prevents the `free-algebras-0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage/-/jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a -> Proxy a) -> Proxy b
foo g = g Proxy
{-# INLINABLE [1] foo #-}
{-# RULES "foo" forall (g :: forall (a :: k). Proxy a -> Proxy a). foo g = g Proxy #-}
```
This typechecks on GHC 8.8.2 and 8.10.1-alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its ill-scoped nature.)
• When checking the transformation rule "foo"
|
10 | {-# RULES "foo" forall (g :: forall (a :: k). Proxy a -> Proxy a). foo g = g Proxy #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/17672Never kick out Given Nominal equalities2021-04-13T14:16:56ZRichard Eisenbergrae@richarde.devNever kick out Given Nominal equalitiesIn other explorations (#17323 and friends) Simon and I determined that a Given Nominal equality should never be kicked out. Why? Because the mutable update of a unification variable should really behave just like a given nominal equality...In other explorations (#17323 and friends) Simon and I determined that a Given Nominal equality should never be kicked out. Why? Because the mutable update of a unification variable should really behave just like a given nominal equality (really, the solver should be pure, but that would be inefficient). Mutable variable updates can't get revisited (i.e. kicked out), so neither should given nominal equalities. And we almost have this property. Here is the relevant text:
Lemma: Nominal Given equalities are never kicked out. Proof: Let `a -fw-> t` be a work item and `b -G/N-> s` be an inert equality. We must show that, regardless of `a`, `t`, `b`, and `s`, condition K from the Note always hold. (Condition K is the "keep" condition.)
K0 is true when `fw /= G/N`. If K0 is true, then K is true, and we are done. So, we assume that `fw = G/N`.
We must show all of K1-K3.
K1: `not (a = b)`. This must be true, because if `a = b`, then `a` would have been rewritten during canonicalization. This is the case because `G/N >= G/N`.
K2: `not (G/N >= G/N) OR G/N >= G/N OR ...`. True by the law of the excluded middle.
K3: Actually, only K3a applies, because the role is nominal: `s /= a`. Actually, we might indeed have `s = a`. But we still shouldn't kick out; see Note \[K3: completeness of solving\], which makes this clear. So, **Action Item**: modify the kick-out conditions so that this proof holds.
QED.
We think the new keep condition should be `s /= a && t /= b`. This ticket is to double-check this intuition and execute.
We believe that there is no loop or other misbehavior here. It's just good hygiene to have given nominals and metavar unifications to be treated identically within the solver. And less kicking out is good, all else being equal.