GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-01-21T11:04:14Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/10321GHC.TypeLits.Nat types no longer fully simplified.2022-01-21T11:04:14ZdarchonGHC.TypeLits.Nat types no longer fully simplified.The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a ...The following code:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
infixr 5 :>
```
when loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:
```
$ ghci example/vec.hs
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a
```
while in GHCi 7.10.1 it gives:
```
$ ghci example/vec.hs
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
That is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.
The same still happens in HEAD (20150417)
```
$ ghci example/vec.hs
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
```
I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.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":"GHC.TypeLits.Nat types no longer fully simplified.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["TypeLits"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata Vec :: Nat -> * -> * where\r\n Nil :: Vec 0 a\r\n (:>) :: a -> Vec n a -> Vec (n + 1) a\r\n\r\ninfixr 5 :>\r\n}}}\r\n\r\nwhen loaded in GHCi 7.8.3, and asking for the type of `(1 :> 2 :> 3 :> Nil)`, gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec 3 a\r\n}}}\r\n\r\nwhile in GHCi 7.10.1 it gives:\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nThat is, the type-level computation, `((0 + 1) + 1) + 1` is only simplified to `2 + 1` in GHC 7.10.1, whereas in 7.8.3 `2+1` was further simplified to `3`.\r\n\r\nThe same still happens in HEAD (20150417)\r\n{{{\r\n$ ghci example/vec.hs \r\nGHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( example/vec.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t (3:>4:>5:>Nil)\r\n(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a\r\n}}}\r\n\r\nI strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/14101Type synonyms can make roles too conservative2022-01-27T07:40:55ZDavid FeuerType synonyms can make roles too conservative```hs
import GHC.Exts
type Arr# = Array#
data Foo a = Foo (Arr# a)
type role Foo representational
```
produces
```
error:
• Role mismatch on variable a:
Annotation says representational but role nominal is required
...```hs
import GHC.Exts
type Arr# = Array#
data Foo a = Foo (Arr# a)
type role Foo representational
```
produces
```
error:
• Role mismatch on variable a:
Annotation says representational but role nominal is required
• while checking a role annotation for ‘Foo’
```
If the type synonym is instead defined
```hs
type Arr# a = Array# a
```
then it works fine.
<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":"Type synonyms can make roles too conservative","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\nimport GHC.Exts\r\n\r\ntype Arr# = Array#\r\n\r\ndata Foo a = Foo (Arr# a)\r\n\r\ntype role Foo representational\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n error:\r\n • Role mismatch on variable a:\r\n Annotation says representational but role nominal is required\r\n • while checking a role annotation for ‘Foo’\r\n}}}\r\n\r\nIf the type synonym is instead defined\r\n\r\n{{{#!hs\r\ntype Arr# a = Array# a\r\n}}}\r\n\r\nthen it works fine.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/21006Unhelpful Kind equality error at the start of file2022-01-28T10:50:09ZJkensikUnhelpful Kind equality error at the start of fileI get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the ...I get an error
```
app\Main.hs:1:1: error:
Couldn't match kind `*' with `Constraint'
When matching types
b :: *
(Set b, Set s) :: Constraint
|
1 | {-# LANGUAGE TypeFamilies #-}
| ^
```
I don't know why b and the constraint (Set b, Set s) are being matched? I would expect the constraint to existentially quantify the type b but why would it be matching them?
I believe the last thing I changed before getting the error was adding OpOutcome to the class.
here is the code
```
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import GHC.TypeLits (Symbol)
import GHC.Exts (Constraint)
import Data.Reflection (Reifies, reflect)
import Data.Proxy (Proxy(..))
main :: IO ()
main = print 5
class ((a,b)::Constraint) => HasCtxt a b
instance (a,b) => HasCtxt a b
class Determines a b | a -> b
instance Determines a b => Determines a b
type Set b = (b ~ b)
type OpLayout a = (forall s ctxt b. (OpCtxt a s b ~ ctxt, Determines a b, Determines a ctxt,Reifies s b) => ( HasCtxt ctxt (Reifies s b))) :: Constraint
data Stack a where
Cons :: OpConstructor a -> Stack b -> Stack a
Nil :: Stack "NIL"
class OpLayout a => OpCode (a::Symbol) where
type OpCtxt a s b = (ctxt :: Constraint) | ctxt -> s b
type OpOutcome a :: *
data OpConstructor a
opValue :: Determines a s => Proxy s
opValue = Proxy
popOP :: OpCtxt a s b => Stack a -> (b :: *)
evalOP :: OpConstructor a -> Stack x -> OpOutcome a
instance OpCode "load_val" where
type OpCtxt "load_val" s b = (Set s, Set b)
type OpOutcome "load_val" = Stack "load_val"
data OpConstructor "load_val" = forall b. LOAD_VAL b
popOP stack = reflect opValue
evalOP op stack = op `Cons` stack
```https://gitlab.haskell.org/ghc/ghc/-/issues/19482"No skolem info" with the infinite kind2022-01-29T16:06:57ZRinat Striungislazybonesxp@gmail.com"No skolem info" with the infinite kind## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from H...## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2847:17 in ghc:GHC.Tc.Errors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Here is my minimal example to reproduce:
```{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Bug where
instance BugClass ((s : sx) :: [r]) where
bugList = testF @r @s
class BugClass k where
bugList :: ()
testF :: forall a (b :: [a]). ()
testF = ()
```
Also, GHC-8.10 works well with a proper error message.
So, it looks like a regression.
## Expected behavior
I should get a compilation error message about the infinite kind construction ( `r ~ [r]`).
## Environment
* GHC version used:
GHC HEAD: [40983d2331fe34c0af6925db7588d5ac6a19ae36](https://gitlab.haskell.org/ghc/ghc/-/tree/40983d2331fe34c0af6925db7588d5ac6a19ae36)9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/20929Different error with representation-polymorphic binder2022-02-03T00:53:58ZKrzysztof GogolewskiDifferent error with representation-polymorphic binderThis program is correctly rejected:
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import GHC.Types
type family Q :: k
type family F :: forall (r :: RuntimeRep) -> TYPE r
f :: Bool
f = let a :: F Q; a = undefined in True
```...This program is correctly rejected:
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import GHC.Types
type family Q :: k
type family F :: forall (r :: RuntimeRep) -> TYPE r
f :: Bool
f = let a :: F Q; a = undefined in True
```
```
• The binder ‘a’ does not have a fixed runtime representation:
F Q :: TYPE Q
```
However, if I change the last line to
```haskell
f = let a :: F r; a = undefined in True
```
I get a different, worse error message:
```
• Expected a type, but ‘F r’ has kind ‘TYPE r’
‘r’ is a rigid type variable bound by
the type signature for ‘a’
at M.hs:10:9-16
```
I'd expect to get the same error in both cases, mentioning no having fixed representation. I suspect there's an extraneous test that is now redundant with the new fixed representation checks.
As far as I can tell, this is not caused by the bug #20837 in `isLiftedType_maybe` - cherry-picking 56e041bb7ac254eaa500317c75731a862cd1ec82 does not solve it.https://gitlab.haskell.org/ghc/ghc/-/issues/21040Curious kind-checking failure with GHC 9.2.1 and visible dependent quantifica...2022-02-04T14:33:59ZRyan ScottCurious kind-checking failure with GHC 9.2.1 and visible dependent quantificationWhile porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTyp...While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
```
```hs
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
```
The `A` module defines two data types, `T1` and `T2`, as well as some functions which use them. The only difference between `T1` and `T2` is that the latter uses visible dependent quantification while the former does not. The `B` module uses these functions in a relatively straightforward way. Note that `B` does _not_ enable `PolyKinds` (I distilled this from a `cabal` project which uses `Haskell2010`).
What's curious about this is that while both `g1` and `g2` will typecheck on GHC 9.0.2, only `g1` typechecks on GHC 9.2.1. On the other hand, `g2` will fail to typecheck in GHC 9.2.1:
```
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
```
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of `NoPolyKinds` might be throwing a wrench into things. Indeed, enabling `PolyKinds` is enough to make the program accepted again. Still, the fact that this _only_ fails if the data type uses visible dependent quantification (and _only_ with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.https://gitlab.haskell.org/ghc/ghc/-/issues/20932Inconsistent tidying of implications2022-02-06T02:53:52ZSimon Peyton JonesInconsistent tidying of implicationsConsider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
...Consider this program (`tcfail013`)
```
f [] = 1
f True = 2
```
We get the unsolved implication
```
Wanted: WC {wc_impl =
Implic {
TcLevel = 1
Skolems = a_aur[sk:1] a_axQ[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_axS} {0}:: Bool ~# [a_aur[sk:1]] (CIrredCan(shape))
[WD] $dNum_axR {0}:: Num a_axQ[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<axY>
the inferred type of f :: [a_aur[sk:1]] -> a_axQ[sk:1] }}
```
Note that the two skolems have the same `OccName`, namely `a`. (They both started life as
unification variablex, which we generalised.)
When we tidy the skolems we get
```
reportImplic
Implic {
TcLevel = 1
Skolems = a_auG[sk:1] a1_ay2[sk:1]
Given-eqs = NoGivenEqs
Status = Insoluble
Given =
Wanted =
WC {wc_simple =
[WD] hole{co_ay4} {0}:: Bool
GHC.Prim.~# [a_auG[sk:1]] (CIrredCan(shape))
[WD] $dNum_ay3 {0}:: Num a_ay2[sk:1] (CDictCan(psc))}
Binds = EvBindsVar<ay9>
the inferred type of f :: [a_auG[sk:1]] -> a1_ay2[sk:1] }
```
We have tidied one `a` to `a`, and the other to `a1`. This flat-out contradicts
`Note [Tidying multiple names at once]` in `GHC.Types.Names.Occurrence` in GHC.Types.Names.Occurrence,
where we say that we should not accidentally privilege one of these 'a's over the others.
The reason we don't follow the standard guidance is that in `reportImplic` we have
```
(env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
scopedSort tvs
```
If instead we had
```
(env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
scopedSort tvs
```
then `tidyVarBndrs` would do the symmetric thing. In our example we'd tidy to `a1` and `a2`.
I think we should do the symmetric thing. But we get a couple of dozen regression failures, as
error messages wibble around. Task: make the change, check the changes, and accept them.
The status quo seems wrong to me.Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21010ASSERTION failure when building subcategories2022-02-08T11:01:59ZMatthew PickeringASSERTION failure when building subcategories```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasC...```
[ 5 of 13] Compiling Control.Subcategory.Bind ( src/Control/Subcategory/Bind.hs, dist/build/Control/Subcategory/Bind.o, dist/build/Control/Subcategory/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```
Which is this assertion in `GHC.Tc.Solver.Canonical.canEqCanLHSFinish`.
```
-- by now, (TyEq:N) is already satisfied (if applicable)
; massert (not bad_newtype)
```
Standalone repro: https://gist.github.com/540cf5453a26825e6885ad59cb01957a
Run using `./run`
```
[nix-shell:~/subcategories-0.1.1.0/repro]$ ./run
[1 of 4] Compiling MonoTraversable ( MonoTraversable.hs, out/MonoTraversable.o, out/MonoTraversable.dyn_o )
[2 of 4] Compiling Internal ( Internal.hs, out/Internal.o, out/Internal.dyn_o )
[3 of 4] Compiling BindA ( BindA.hs, out/BindA.o, out/BindA.dyn_o )
[4 of 4] Compiling Bind ( Bind.hs, out/Bind.o, out/Bind.dyn_o )
<no location info>: error:
ASSERT failed!
CallStack (from HasCallStack):
massert, called at compiler/GHC/Tc/Solver/Canonical.hs:2485:10 in ghc:GHC.Tc.Solver.Canonical
```https://gitlab.haskell.org/ghc/ghc/-/issues/20894GHC 9.2 creates an unsafe coercion between a boxed and an unboxed type2022-02-09T16:26:28Zsheafsam.derbyshire@gmail.comGHC 9.2 creates an unsafe coercion between a boxed and an unboxed typeThe attached file (a single module with no dependencies, but unfortunately a bit long/complex) causes a Core Lint error on GHC 9.2. Compile with `-O1 -dcore-lint`.
GHC 9.0 and GHC HEAD both seem to not be affected.
```
warning:
...The attached file (a single module with no dependencies, but unfortunately a bit long/complex) causes a Core Lint error on GHC 9.2. Compile with `-O1 -dcore-lint`.
GHC 9.0 and GHC HEAD both seem to not be affected.
```
warning:
Unsafe coercion: between unboxed and boxed value
From: ()
To: Int#
```
[Bug.hs](/uploads/45e865bdbcd94302b9f6fcd45bd93005/Bug.hs)
In the `dump-ds-preopt` output I am seeing some worrying coercions, e.g.
```haskell
$d~_a1c4 :: MyInt ~ 'LitTy
[LclId]
$d~_a1c4
= GHC.Types.Eq#
@(Type 'KEmpty 'Type)
@MyInt
@'LitTy
@~(<'LitTy>_N :: 'LitTy GHC.Prim.~# 'LitTy)
```
but here the promoted `LitTy` constructor is insufficiently applied. It seems that the definition of the promoted data constructor `LitTy` confuses GHC, as it only takes invisible arguments.
I haven't investigated further or identified which commits broke or fixed this yet. @rae?9.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/9805Use TrieMaps to speed up type class instance lookup2022-02-09T17:33:57ZEdward Z. YangUse TrieMaps to speed up type class instance lookupCurrently, type class instance resolution is performed by doing a map lookup by type class, and then linearly matching against every instance. This is not great, and for a while, simonpj has been keen on using the TrieMap data structure ...Currently, type class instance resolution is performed by doing a map lookup by type class, and then linearly matching against every instance. This is not great, and for a while, simonpj has been keen on using the TrieMap data structure in GHC, which has been previously used to implement a map from CoreExprs to various things (e.g. for CSE). What makes this a little tricky is that instance lookup isn't intended to be an exact match: we should unify so-called template variables and provide a substitution; furthermore, there may be multiple matches.
After some prototyping, I think we should be able to make this work. The primary refactoring we have to do is \*maintain the key associated with an entry in a TrieMap\*. Unlike the current uses of TrieMaps, where it's acceptable to lose the underlying key associated with an entry in the TrieMap, we need to know the key when doing unification, because it may be reported in the substitution. There are a few knock-on effects of this:
- We should add a method `foldWithKeyTM :: (Key m -> a -> b -> b) -> m a -> b -> b` to the `TrieMap` type class.
- We need a variant of `UniqFM` which tracks the original key that was used. I propose we name it `UniqKM` (unique key map). A number of implementations of `TrieMap` need to be adjusted to use this instead of `UniqFM`.
- Why can't we just represent keyed TrieMaps as `TypeMap (Type, a)`? It might be possible. An insurmountable difficulty would be if we need to know the partial key PRIOR to having finished traversing the TrieMap; however, for the parts of the unification algorithm I've implemented, this does not seem to be the case. The primary actual difficulty is that `Type` uses a named representation, whereas `TypeMap` keys are on-the-fly deBruijn numbered. There would at least be some annoying fiddliness.
- Reversing the deBruijn numbered key into a `Type` is a bit goofy. Essentially, you need the reverse of the current `CmEnv`: a mapping from de Bruijn levels to the `Var` you've decided to allocate. (I've called this `CfEnv` in my prototype)
- When we represent a TrieMap binder, we have to put the binder map on the OUTSIDE, as opposed to the inside as it is currently. Otherwise, we can't update the `CfEnv` with the new mapping before making the recursive call to fold-with-key.
I'll attach the standalone Haskell file I used to prototype this, wherein I copy-pasted a lot of Haskell from GHC's source and implemented fuzzy map on a simplified version of `Type`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Use TrieMaps to speed up type class instance lookup","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"ezyang"},"version":"7.9","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Task","description":"Currently, type class instance resolution is performed by doing a map lookup by type class, and then linearly matching against every instance. This is not great, and for a while, simonpj has been keen on using the TrieMap data structure in GHC, which has been previously used to implement a map from CoreExprs to various things (e.g. for CSE). What makes this a little tricky is that instance lookup isn't intended to be an exact match: we should unify so-called template variables and provide a substitution; furthermore, there may be multiple matches.\r\n\r\nAfter some prototyping, I think we should be able to make this work. The primary refactoring we have to do is *maintain the key associated with an entry in a TrieMap*. Unlike the current uses of TrieMaps, where it's acceptable to lose the underlying key associated with an entry in the TrieMap, we need to know the key when doing unification, because it may be reported in the substitution. There are a few knock-on effects of this:\r\n\r\n * We should add a method `foldWithKeyTM :: (Key m -> a -> b -> b) -> m a -> b -> b` to the `TrieMap` type class.\r\n * We need a variant of `UniqFM` which tracks the original key that was used. I propose we name it `UniqKM` (unique key map). A number of implementations of `TrieMap` need to be adjusted to use this instead of `UniqFM`.\r\n * Why can't we just represent keyed TrieMaps as `TypeMap (Type, a)`? It might be possible. An insurmountable difficulty would be if we need to know the partial key PRIOR to having finished traversing the TrieMap; however, for the parts of the unification algorithm I've implemented, this does not seem to be the case. The primary actual difficulty is that `Type` uses a named representation, whereas `TypeMap` keys are on-the-fly deBruijn numbered. There would at least be some annoying fiddliness.\r\n * Reversing the deBruijn numbered key into a `Type` is a bit goofy. Essentially, you need the reverse of the current `CmEnv`: a mapping from de Bruijn levels to the `Var` you've decided to allocate. (I've called this `CfEnv` in my prototype)\r\n * When we represent a TrieMap binder, we have to put the binder map on the OUTSIDE, as opposed to the inside as it is currently. Otherwise, we can't update the `CfEnv` with the new mapping before making the recursive call to fold-with-key.\r\n\r\nI'll attach the standalone Haskell file I used to prototype this, wherein I copy-pasted a lot of Haskell from GHC's source and implemented fuzzy map on a simplified version of `Type`.","type_of_failure":"OtherFailure","blocking":[]} -->Edward Z. YangEdward Z. Yanghttps://gitlab.haskell.org/ghc/ghc/-/issues/20933matchInstEnv accounts for 50% of typechecker time2022-02-09T17:33:58ZMatthew PickeringmatchInstEnv accounts for 50% of typechecker time![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent type...![2022-01-11-120537_1838x781](/uploads/54981218c0deaf225d86e747e120fcbf/2022-01-11-120537_1838x781.png)
I created a profile of GHC compiling a large commercial project and noticed that `matchInstEnv` accounted for 50% of time spent typechecking the project. That seems like rather a lot. Zooming into just `matchInstEnv`..
![2022-01-11-120754_1917x288](/uploads/caa8b8a41042b4725d2a3685652b00ad/2022-01-11-120754_1917x288.png)
It seems that the cost is split quite evenly between `tc_unify_tys_fg`, `tc_match_tys` and `$instIsVisible`, `instIsVisible` looks quite cheap so I wondered if this function is getting hammered an ungodly number of times.https://gitlab.haskell.org/ghc/ghc/-/issues/20527GHC 9.2 rejects certain poly-kinded unlifted newtype instances2022-02-13T02:59:37Zsheafsam.derbyshire@gmail.comGHC 9.2 rejects certain poly-kinded unlifted newtype instancesThe following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUA...The following program compiles on GHC 9.0, but on GHC 9.2 and HEAD it produces an error.
```haskell
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedNewtypes #-}
module NewtypeInstance where
import GHC.Exts
type DF :: TYPE r
data family DF
newtype instance DF = MkDF1 Int
newtype instance DF = MkDF2 Int#
newtype instance DF = MkDF3 (# Int#, Int, Word #)
newtype instance DF = MKDF4 (# (# #) | Float# #)
```
```
NewtypeInstance.hs:15:29: error:
* Expecting a lifted type, but `Int#' is unlifted
* In the type `Int#'
In the definition of data constructor `MkDF2'
In the newtype instance declaration for `DF'
|
15 | newtype instance DF = MkDF2 Int#
| ^^^^
NewtypeInstance.hs:16:29: error:
* Expecting a lifted type, but `(# Int#, Int, Word #)' is unlifted
* In the type `(# Int#, Int, Word #)'
In the definition of data constructor `MkDF3'
In the newtype instance declaration for `DF'
|
16 | newtype instance DF = MkDF3 (# Int#, Int, Word #)
| ^^^^^^^^^^^^^^^^^^^^^
NewtypeInstance.hs:17:29: error:
* Expecting a lifted type, but `(# (# #) | Float# #)' is unlifted
* In the type `(# (# #) | Float# #)'
In the definition of data constructor `MKDF4'
In the newtype instance declaration for `DF'
|
17 | newtype instance DF = MKDF4 (# (# #) | Float# #)
| ^^^^^^^^^^^^^^^^^^^^
```
I think the program should be accepted: we have an invisible kind argument which is taking a different value in each newtype instance. For some reason, starting with GHC 9.2, some defaulting seems to take place and we start expecting `r` to be `LiftedRep`.
I'm not sure what has caused the change in behaviour. Pinging the experts @rae and @RyanGlScott.9.2.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21038GHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskell2022-02-14T13:59:23ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes and TemplateHaskellWhile porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell...While porting some code over to use GHC 9.2.1, I noticed a typechecking regression that doesn't appear to be explained in the 9.2.1 release notes. Here is a minimal example:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo $ \x -> x
worksOnAllGHCs3 :: Foo
worksOnAllGHCs3 = $([| MkFoo |]) (\x -> x)
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
```
All four of these top-level functions will typecheck on GHC 9.0.2 and earlier. On GHC 9.2.1 and HEAD, `worksOnAllGHCs{1,2,3}` functions will typecheck, but the `doesn'tWorkOnGHC9'2` function will not typecheck:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo)’
In the expression: (MkFoo) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo |]) $ \x -> x
| ^^^^^^^^^^^^^
```
I'm unclear why using a Template Haskell splice would affect typechecking like this, so I believe this is a bug.9.2.2Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/8392Suggest AllowAmbiguousTypes2022-02-15T18:30:18ZrwbartonSuggest AllowAmbiguousTypesThe error message I get with GHC HEAD on the example program in #8390:
```
tf.hs:38:10:
Could not deduce (Fun g a b0)
arising from the ambiguity check for an instance declaration
from the context (Fun f b c, Fun g a b)
...The error message I get with GHC HEAD on the example program in #8390:
```
tf.hs:38:10:
Could not deduce (Fun g a b0)
arising from the ambiguity check for an instance declaration
from the context (Fun f b c, Fun g a b)
bound by an instance declaration:
(Fun f b c, Fun g a b) => Fun (Compose f g) a c
at tf.hs:38:10-56
The type variable ‛b0’ is ambiguous
In the ambiguity check for:
forall f g a c b. (Fun f b c, Fun g a b) => Fun (Compose f g) a c
In the instance declaration for ‛Fun (Compose f g) a c’
```
could perhaps benefit from an appended line:
```
(To defer this ambiguity check to use sites, enable AllowAmbiguousTypes)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | FeatureRequest |
| 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":"Suggest AllowAmbiguousTypes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The error message I get with GHC HEAD on the example program in #8390:\r\n{{{\r\ntf.hs:38:10:\r\n Could not deduce (Fun g a b0)\r\n arising from the ambiguity check for an instance declaration\r\n from the context (Fun f b c, Fun g a b)\r\n bound by an instance declaration:\r\n (Fun f b c, Fun g a b) => Fun (Compose f g) a c\r\n at tf.hs:38:10-56\r\n The type variable ‛b0’ is ambiguous\r\n In the ambiguity check for:\r\n forall f g a c b. (Fun f b c, Fun g a b) => Fun (Compose f g) a c\r\n In the instance declaration for ‛Fun (Compose f g) a c’\r\n}}}\r\ncould perhaps benefit from an appended line:\r\n{{{\r\n (To defer this ambiguity check to use sites, enable AllowAmbiguousTypes)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/14916Missing checks when deriving special classes2022-02-16T12:06:47ZAndres LöhMissing checks when deriving special classesFor the following program
```hs
{-# LANGUAGE DeriveAnyClass #-}
module T where
import Data.Coerce
import Data.Typeable
data A = MkA deriving ((~) A)
data B = MkB deriving (Coercible B)
```
the deriving clause for `A` is accepted with...For the following program
```hs
{-# LANGUAGE DeriveAnyClass #-}
module T where
import Data.Coerce
import Data.Typeable
data A = MkA deriving ((~) A)
data B = MkB deriving (Coercible B)
```
the deriving clause for `A` is accepted without complaints, and the
deriving clause for `B` fails with the following error:
```
T.hs:8:24: error:
Top-level bindings for unlifted types aren't allowed:
|
8 | data B = MkB deriving (Coercible B)
| ^^^^^^^^^^^
```
Corresponding standalone deriving instances trigger errors
saying "Manual instances of this class are not permitted".
Probably similar error messages should be triggered here.8.4.2https://gitlab.haskell.org/ghc/ghc/-/issues/20921Regression in ambiguity checking for partial type signatures in GHC 9.22022-02-21T11:13:10Zsheafsam.derbyshire@gmail.comRegression in ambiguity checking for partial type signatures in GHC 9.2The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ...The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PsigBug where
import Data.Kind
( Constraint )
import GHC.TypeLits
( ErrorMessage(..), TypeError )
import GHC.TypeNats ( Nat )
type family OK (i :: Nat) :: Constraint where
OK 1 = ()
OK 2 = ()
OK n = TypeError (ShowType n :<>: Text "is not OK")
class C (i :: Nat) where
foo :: Int
instance C 1 where
foo = 1
instance C 2 where
foo = 2
type family Boo (i :: Nat) :: Nat where
Boo i = i
bar :: Int
bar =
let
quux :: forall (i :: Nat). ( OK (Boo i), _ ) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
```
```
PsigBug.hs:38:5: error:
* Could not deduce: OK i0
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
PsigBug.hs:38:5: error:
* Could not deduce (C i0)
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
The type variable `i0' is ambiguous
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
```
These messages mention an ambiguous variable `i0`... but it doesn't actually appear anywhere in the rest of the messages!
This bug prevents one of my libraries from compiling (and I couldn't find a workaround), so this is not only of theoretical interest.9.2.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/19677GHC does not rewrite in FunTy2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.devGHC does not rewrite in FunTyConsider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
...Consider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
```
GHC rejects, saying it cannot find an instance for `C (a -> b)`. But it should accept.
The problem is that the kinds of `a` and `b` are `TYPE (Lifty i)`. Even if we know `i ~ Int`, and therefore that `Lifty i ~ LiftedRep`, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477, when complete, should address this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/10431EqualityConstraints extension?2022-02-23T02:01:05ZAdam GundryEqualityConstraints extension?At the moment, writing an equality constraint in a type requires at least one of the `GADTs` or `TypeFamilies` extensions. However, each of these has other effects. Could we have an `EqualityConstraints` extension to permit equality cons...At the moment, writing an equality constraint in a type requires at least one of the `GADTs` or `TypeFamilies` extensions. However, each of these has other effects. Could we have an `EqualityConstraints` extension to permit equality constraints in types, but neither GADTs nor type families? Presumably this extension should imply `MonoLocalBinds`.
The `GADTs` extension could then become precisely the conjunction of `GADTSyntax`, `EqualityConstraints` and `ExistentialQuantification`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| 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":"EqualityConstraints extension?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.12.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"At the moment, writing an equality constraint in a type requires at least one of the `GADTs` or `TypeFamilies` extensions. However, each of these has other effects. Could we have an `EqualityConstraints` extension to permit equality constraints in types, but neither GADTs nor type families? Presumably this extension should imply `MonoLocalBinds`.\r\n\r\nThe `GADTs` extension could then become precisely the conjunction of `GADTSyntax`, `EqualityConstraints` and `ExistentialQuantification`.","type_of_failure":"OtherFailure","blocking":[]} -->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/19131Does the sub-type check in Note [Impedance matching] ever fail?2022-02-23T13:21:43ZRichard Eisenbergrae@richarde.devDoes the sub-type check in Note [Impedance matching] ever fail?`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a -> Bool -> Bool
g_m...`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a -> Bool -> Bool
g_mono_ty :: [b] -> Bool -> Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
g :: forall b. [b] -> Bool -> Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a -> F a
where F is a non-injective type function.
```
This describes a sub-type check. That sub-type check is performed with the context returned from this function:
```hs
mk_impedance_match_msg :: MonoBindInfo
-> TcType -> TcType
-> TidyEnv -> TcM (TidyEnv, SDoc)
-- This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing -> text "inferred"
Just sig | isPartialSig sig -> text "(partial)"
| otherwise -> empty
```
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this sub-type check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.