GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210118T17:11:59Zhttps://gitlab.haskell.org/ghc/ghc//issues/19197‘:kind () :: '()’ doesn't give any output20210118T17:11:59ZIcelandjack‘:kind () :: '()’ doesn't give any output```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an error```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an errorhttps://gitlab.haskell.org/ghc/ghc//issues/19196TypeInType prevents Typeable from being resolved from a given20210111T03:19:52ZSerge KosyrevTypeInType prevents Typeable from being resolved from a givenThe following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE UndecidableInstances #}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t > LTag (Live t)
reconstruct :: Dynamic > LTag l > ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) >
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:1925
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:1017
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:1656
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))

26  (fromDynamic dyn :: Maybe (IOA (Live t)))
 ^^^^^^^^^^^^^^^
```
Potentially related to #16627The following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE UndecidableInstances #}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t > LTag (Live t)
reconstruct :: Dynamic > LTag l > ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) >
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:1925
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 > LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:1017
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:1656
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))

26  (fromDynamic dyn :: Maybe (IOA (Live t)))
 ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc//issues/19167Regression around overloaded literals and type applications20210115T08:50:06ZRichard Eisenbergrae@richarde.devRegression around overloaded literals and type applicationsThe new eager instantiation approach (adopted as a part of Quick Look) does not treat overloaded literals as "heads". This causes trouble when using them with type applications, which can be useful when using `XRebindableSyntax`. Specifically, the following module compiles with released GHCs:
```hs
{# LANGUAGE RebindableSyntax, RankNTypes, TypeApplications, OverloadedStrings,
OverloadedLists, TypeFamilies #}
module Bug where
import qualified Prelude as P
import qualified GHC.Exts as P
import Data.List.NonEmpty ( NonEmpty )
fromInteger :: P.Integer > forall a. P.Num a => a
fromInteger n = P.fromInteger n
shouldBeAnInt = 3 @P.Int
newtype RevString = RevString P.String
deriving P.Show
instance P.IsString RevString where
fromString str = RevString (P.reverse str)
fromString :: P.String > forall a. P.IsString a => a
fromString str = P.fromString str
shouldBeARevString = "hello" @RevString
fromListN :: P.Int > [elt] > forall list. (P.IsList list, elt ~ P.Item list) => list
fromListN n l = P.fromListN n l
shouldBeANonEmpty = ['x', 'y', 'z'] @(NonEmpty P.Char)
```
All three `shouldBe` definitions are rejected with HEAD. But accepted by 8.xThe new eager instantiation approach (adopted as a part of Quick Look) does not treat overloaded literals as "heads". This causes trouble when using them with type applications, which can be useful when using `XRebindableSyntax`. Specifically, the following module compiles with released GHCs:
```hs
{# LANGUAGE RebindableSyntax, RankNTypes, TypeApplications, OverloadedStrings,
OverloadedLists, TypeFamilies #}
module Bug where
import qualified Prelude as P
import qualified GHC.Exts as P
import Data.List.NonEmpty ( NonEmpty )
fromInteger :: P.Integer > forall a. P.Num a => a
fromInteger n = P.fromInteger n
shouldBeAnInt = 3 @P.Int
newtype RevString = RevString P.String
deriving P.Show
instance P.IsString RevString where
fromString str = RevString (P.reverse str)
fromString :: P.String > forall a. P.IsString a => a
fromString str = P.fromString str
shouldBeARevString = "hello" @RevString
fromListN :: P.Int > [elt] > forall list. (P.IsList list, elt ~ P.Item list) => list
fromListN n l = P.fromListN n l
shouldBeANonEmpty = ['x', 'y', 'z'] @(NonEmpty P.Char)
```
All three `shouldBe` definitions are rejected with HEAD. But accepted by 8.xhttps://gitlab.haskell.org/ghc/ghc//issues/19154GHC 9.0 no longer typechecks a program involving overloaded labels and type a...20210112T22:00:26ZsheafGHC 9.0 no longer typechecks a program involving overloaded labels and type applicationsIn the program that follows, I specify the type of a label by using a visible type application.
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE OverloadedLabels #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RebindableSyntax #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Labels where
 base
import Prelude
import Data.Kind
( Type )
import GHC.TypeLits
( Symbol, KnownSymbol )

data Label (k :: Symbol) (a :: Type) = Label
class IsLabel k a v  v > a, v > k where
fromLabel :: v
instance KnownSymbol k => IsLabel k a (Label k a) where
fromLabel = Label @k @a
foo :: Label k a > ()
foo _ = ()
test :: ()
test = foo ( #label @Bool )
```
The point of this program is that the label `#label` is polymorphic:
```haskell
#label :: forall (a :: Type). Label "label" a
```
and I am able to instantiate the type variable `a` with a type application.
<p>
<details>
<summary> Show/hide further context.</summary>
This was boiled down from the overloaded label syntax I provide in my shader library, see [here](https://gitlab.com/sheaf/fir//blob/master/src/FIR/Syntax/Labels.hs).
This added bit of syntax allows users of the library to write shaders in an imperative style, see [here](https://gitlab.com/sheaf/fir//blob/master/firexamples/examples/shaders/FIR/Examples/JuliaSet/Shaders.hs#L117) for an example.
</details>
</p>
This program compiles fine on GHC 8.10 (and previous GHC versions), but fails to compile on GHC 9.0 (rc1) with the following error:
```
Labels.hs:35:14: error:
* Cannot apply expression of type `v0'
to a visible type argument `Bool'
* In the first argument of `foo', namely `(#label @Bool)'
In the expression: foo (#label @Bool)
In an equation for `test': test = foo (#label @Bool)

35  test = foo ( #label @Bool )
 ^^^^^
```
Can someone enlighten me about what's going on? I found it quite useful to be able to pass further arguments to an overloaded label in this way, whereas I now have to write something like
```haskell
test :: ()
test = foo ( #label :: Label _ Bool )
```
to specify `a`, which defeats the purpose of the overloaded labels syntax. At that point I might as well just write:
```haskell
foo ( Label @"label" @Bool )
```In the program that follows, I specify the type of a label by using a visible type application.
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE OverloadedLabels #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RebindableSyntax #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Labels where
 base
import Prelude
import Data.Kind
( Type )
import GHC.TypeLits
( Symbol, KnownSymbol )

data Label (k :: Symbol) (a :: Type) = Label
class IsLabel k a v  v > a, v > k where
fromLabel :: v
instance KnownSymbol k => IsLabel k a (Label k a) where
fromLabel = Label @k @a
foo :: Label k a > ()
foo _ = ()
test :: ()
test = foo ( #label @Bool )
```
The point of this program is that the label `#label` is polymorphic:
```haskell
#label :: forall (a :: Type). Label "label" a
```
and I am able to instantiate the type variable `a` with a type application.
<p>
<details>
<summary> Show/hide further context.</summary>
This was boiled down from the overloaded label syntax I provide in my shader library, see [here](https://gitlab.com/sheaf/fir//blob/master/src/FIR/Syntax/Labels.hs).
This added bit of syntax allows users of the library to write shaders in an imperative style, see [here](https://gitlab.com/sheaf/fir//blob/master/firexamples/examples/shaders/FIR/Examples/JuliaSet/Shaders.hs#L117) for an example.
</details>
</p>
This program compiles fine on GHC 8.10 (and previous GHC versions), but fails to compile on GHC 9.0 (rc1) with the following error:
```
Labels.hs:35:14: error:
* Cannot apply expression of type `v0'
to a visible type argument `Bool'
* In the first argument of `foo', namely `(#label @Bool)'
In the expression: foo (#label @Bool)
In an equation for `test': test = foo (#label @Bool)

35  test = foo ( #label @Bool )
 ^^^^^
```
Can someone enlighten me about what's going on? I found it quite useful to be able to pass further arguments to an overloaded label in this way, whereas I now have to write something like
```haskell
test :: ()
test = foo ( #label :: Label _ Bool )
```
to specify `a`, which defeats the purpose of the overloaded labels syntax. At that point I might as well just write:
```haskell
foo ( Label @"label" @Bool )
```https://gitlab.haskell.org/ghc/ghc//issues/19142panic lookup_final_id with fdefertypeerrors and kind error in instance def...20210121T20:16:21ZJakob Brünkerpanic lookup_final_id with fdefertypeerrors and kind error in instance definition## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/19140panic: No skolem info when trying to use variable with polymorphic kind as Ty...20201231T13:44:07ZJakob Brünkerpanic: No skolem info when trying to use variable with polymorphic kind as Type/Constraint## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the following three instances trigger the error
```haskell
{# LANGUAGE ExplicitForAll , PolyKinds #}
instance (forall (a :: k) . a) => Show b
instance (forall (a :: k) . Show a) => Show b
instance (forall (a :: k) . a > a) => Show b
```
Error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
No skolem info:
[k_aEZ[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
8.10 has the expected behavior: show the following type error
```
Bug.hs:3:29: error:
• Expected a constraint, but ‘a’ has kind ‘k’
• In the instance declaration for ‘Show b’

3  instance (forall (a :: k) . a) => Show b
 ^
Bug.hs:4:34: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the first argument of ‘Show’, namely ‘a’
In the instance declaration for ‘Show b’

4  instance (forall (a :: k) . Show a) => Show b
 ^
Bug.hs:5:29: error:
• Expected a constraint, but ‘a > a’ has kind ‘*’
• In the instance declaration for ‘Show b’

5  instance (forall (a :: k) . a > a) => Show b
 ^^^^^^
Failed, no modules loaded.
```
## Environment
* GHC version used: 9.0.0.20201227
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the following three instances trigger the error
```haskell
{# LANGUAGE ExplicitForAll , PolyKinds #}
instance (forall (a :: k) . a) => Show b
instance (forall (a :: k) . Show a) => Show b
instance (forall (a :: k) . a > a) => Show b
```
Error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
No skolem info:
[k_aEZ[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
8.10 has the expected behavior: show the following type error
```
Bug.hs:3:29: error:
• Expected a constraint, but ‘a’ has kind ‘k’
• In the instance declaration for ‘Show b’

3  instance (forall (a :: k) . a) => Show b
 ^
Bug.hs:4:34: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the first argument of ‘Show’, namely ‘a’
In the instance declaration for ‘Show b’

4  instance (forall (a :: k) . Show a) => Show b
 ^
Bug.hs:5:29: error:
• Expected a constraint, but ‘a > a’ has kind ‘*’
• In the instance declaration for ‘Show b’

5  instance (forall (a :: k) . a > a) => Show b
 ^^^^^^
Failed, no modules loaded.
```
## Environment
* GHC version used: 9.0.0.20201227
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_649.2.1https://gitlab.haskell.org/ghc/ghc//issues/19137Incorrect documentation around EqualCtList20201230T19:59:58ZRichard Eisenbergrae@richarde.devIncorrect documentation around EqualCtListThe solver maintains a structure `EqualCtList`, with this Note:
```
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* All are equalities
* All these equalities have the same LHS
* The list is never empty
* No element of the list can rewrite any other
* Derived before Wanted
From the fourth invariant it follows that the list is
 A single [G], or
 Zero or one [D] or [WD], followed by any number of [W]
The Wanteds can't rewrite anything which is why we put them last
```
Yet this isn't quite accurate. If we have a `[G] a ~R Bool` and a `[D] a ~ Int`, neither can rewrite the other. Both can live in the `EqualCtList` quite peacefully. Thus, the "it follows that" is wrong. Worse, the rewriter contains the code
```hs
; case lookupDVarEnv ieqs tv of
Just (EqualCtList (ct : _))  If the first doesn't work,
 the subsequent ones won't either
 CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } < ct
```
but the comment there isn't true: the first might not work, but maybe a later one will.
I tried quite hard to come up with some misbehavior that this misunderstanding caused, but it's quite hard. An example with a Given that contains a touchable metavariable wouldn't be convincing (#18929), and all other examples seem to lead to program rejection. And because the prioritization of some errors over others, it's hard to see the bad error.
Yet I still think there is a problem here, and that we should search through the list looking for a valid inert.The solver maintains a structure `EqualCtList`, with this Note:
```
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* All are equalities
* All these equalities have the same LHS
* The list is never empty
* No element of the list can rewrite any other
* Derived before Wanted
From the fourth invariant it follows that the list is
 A single [G], or
 Zero or one [D] or [WD], followed by any number of [W]
The Wanteds can't rewrite anything which is why we put them last
```
Yet this isn't quite accurate. If we have a `[G] a ~R Bool` and a `[D] a ~ Int`, neither can rewrite the other. Both can live in the `EqualCtList` quite peacefully. Thus, the "it follows that" is wrong. Worse, the rewriter contains the code
```hs
; case lookupDVarEnv ieqs tv of
Just (EqualCtList (ct : _))  If the first doesn't work,
 the subsequent ones won't either
 CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } < ct
```
but the comment there isn't true: the first might not work, but maybe a later one will.
I tried quite hard to come up with some misbehavior that this misunderstanding caused, but it's quite hard. An example with a Given that contains a touchable metavariable wouldn't be convincing (#18929), and all other examples seem to lead to program rejection. And because the prioritization of some errors over others, it's hard to see the bad error.
Yet I still think there is a problem here, and that we should search through the list looking for a valid inert.https://gitlab.haskell.org/ghc/ghc//issues/19131Does the subtype check in Note [Impedance matching] ever fail?20201229T15:38:12ZRichard Eisenbergrae@richarde.devDoes the subtype 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_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 noninjective type function.
```
This describes a subtype check. That subtype 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 subtype 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.`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 noninjective type function.
```
This describes a subtype check. That subtype 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 subtype 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.https://gitlab.haskell.org/ghc/ghc//issues/19107GADT pattern match defeats instance solving20210116T04:14:24ZRichard Eisenbergrae@richarde.devGADT pattern match defeats instance solvingWhen I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.When I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19106Partial type signature variable confuses instance solving20210116T04:14:24ZRichard Eisenbergrae@richarde.devPartial type signature variable confuses instance solvingWhen I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.When I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19060Make the canonicaliser do unification20201214T15:23:24ZSimon Peyton JonesMake the canonicaliser do unificationLook at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `checkTyVarEq`
* All this just gets the orientation right. Then we forget all that, and later, in `tryToSolveByUnification` we call `unifyTest` again. What a mess.
One thing that discouraged me was the miasma of `rewriteEqEvidence` and `rewriteCastedEquality` and doswap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.Look at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `checkTyVarEq`
* All this just gets the orientation right. Then we forget all that, and later, in `tryToSolveByUnification` we call `unifyTest` again. What a mess.
One thing that discouraged me was the miasma of `rewriteEqEvidence` and `rewriteCastedEquality` and doswap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.https://gitlab.haskell.org/ghc/ghc//issues/19051Allow named wildcards in constraints20201223T15:23:55ZsheafAllow named wildcards in constraints```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)https://gitlab.haskell.org/ghc/ghc//issues/19044Regression: HEAD requires FlexibleContexts because of inferred, redundant con...20201219T14:16:12ZRyan ScottRegression: HEAD requires FlexibleContexts because of inferred, redundant constraint_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7287)._
The following code, minimized from the `pandoc2.11.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b where
m :: a > b
instance C a a where
m = id
instance C a (Maybe a) where
m _ = Nothing
f :: a > Maybe a
f = g
where
g x = h (m x) x
h :: Maybe a > a > Maybe a
h = const
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc9.1.0.20201208/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:17:5: error:
• Non typevariable argument in the constraint: C a1 (Maybe a1)
(Use FlexibleContexts to permit this)
• When checking the inferred type
g :: forall {a}. C a (Maybe a) => a > Maybe a
In an equation for ‘f’:
f = g
where
g x = h (m x) x

17  g x = h (m x) x
 ^^^^^^^^^^^^^^^
```
Previous versions of GHC would accept this program because the inferred type of `g` was `forall {a}. a > Maybe a`, not `g :: forall {a}. C a (Maybe a) => a > Maybe a`. The presence of this extra `C a (Maybe a)` constraint (which seems redundant?) is suspicious, so I opted to open an issue about it._Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7287)._
The following code, minimized from the `pandoc2.11.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b where
m :: a > b
instance C a a where
m = id
instance C a (Maybe a) where
m _ = Nothing
f :: a > Maybe a
f = g
where
g x = h (m x) x
h :: Maybe a > a > Maybe a
h = const
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc9.1.0.20201208/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:17:5: error:
• Non typevariable argument in the constraint: C a1 (Maybe a1)
(Use FlexibleContexts to permit this)
• When checking the inferred type
g :: forall {a}. C a (Maybe a) => a > Maybe a
In an equation for ‘f’:
f = g
where
g x = h (m x) x

17  g x = h (m x) x
 ^^^^^^^^^^^^^^^
```
Previous versions of GHC would accept this program because the inferred type of `g` was `forall {a}. a > Maybe a`, not `g :: forall {a}. C a (Maybe a) => a > Maybe a`. The presence of this extra `C a (Maybe a)` constraint (which seems redundant?) is suspicious, so I opted to open an issue about it.9.2.1https://gitlab.haskell.org/ghc/ghc//issues/19042Regression: HEAD incurs a reduction stack overflow on program involving type ...20210115T03:25:35ZRyan ScottRegression: HEAD incurs a reduction stack overflow on program involving type equality_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7936)._
The following code, minimized from the `plots0.1.1.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Plots.Types where
import Data.Functor
import Data.Typeable
type family N a
data StyledPlot n where
StyledPlot :: Typeable p => p > StyledPlot (N p)
styledPlot :: forall p f.
(Typeable p, Applicative f)
=> (p > f p)
> StyledPlot (N p) > f (StyledPlot (N p))
styledPlot f s@(StyledPlot p) =
case eq p of
Just Refl > f p <&> \p' > StyledPlot p'
Nothing > pure s
where eq :: Typeable a => a > Maybe (a :~: p)
eq _ = eqT
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Plots.Types ( Bug.hs, Bug.o )
Bug.hs:21:33: error:
• Reduction stack overflow; size = 201
When simplifying the following type: N p1
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: StyledPlot p'
In the second argument of ‘(<&>)’, namely ‘\ p' > StyledPlot p'’
In the expression: f p <&> \ p' > StyledPlot p'

21  Just Refl > f p <&> \p' > StyledPlot p'
 ^^^^^^^^^^^^^
```_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7936)._
The following code, minimized from the `plots0.1.1.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Plots.Types where
import Data.Functor
import Data.Typeable
type family N a
data StyledPlot n where
StyledPlot :: Typeable p => p > StyledPlot (N p)
styledPlot :: forall p f.
(Typeable p, Applicative f)
=> (p > f p)
> StyledPlot (N p) > f (StyledPlot (N p))
styledPlot f s@(StyledPlot p) =
case eq p of
Just Refl > f p <&> \p' > StyledPlot p'
Nothing > pure s
where eq :: Typeable a => a > Maybe (a :~: p)
eq _ = eqT
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Plots.Types ( Bug.hs, Bug.o )
Bug.hs:21:33: error:
• Reduction stack overflow; size = 201
When simplifying the following type: N p1
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: StyledPlot p'
In the second argument of ‘(<&>)’, namely ‘\ p' > StyledPlot p'’
In the expression: f p <&> \ p' > StyledPlot p'

21  Just Refl > f p <&> \p' > StyledPlot p'
 ^^^^^^^^^^^^^
```9.2.1https://gitlab.haskell.org/ghc/ghc//issues/19013Type wildcard infers differently than no type signature20201210T00:22:10ZdminuosoType wildcard infers differently than no type signature```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.https://gitlab.haskell.org/ghc/ghc//issues/19010Partial type signature algorithm fails to infer constraints in the presence o...20201220T03:26:43ZsheafPartial type signature algorithm fails to infer constraints in the presence of GADTsI've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).I've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).https://gitlab.haskell.org/ghc/ghc//issues/18987Quick Look does not zonk return types20201221T11:00:00ZRichard Eisenbergrae@richarde.devQuick Look does not zonk return typesTest case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.Test case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.https://gitlab.haskell.org/ghc/ghc//issues/18929Investigate touchable metavariables in Givens20210102T14:14:41ZRichard Eisenbergrae@richarde.devInvestigate touchable metavariables in Givens@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.https://gitlab.haskell.org/ghc/ghc//issues/18920ghc8.8 does not infer kind20201109T14:13:59Zjwaldmannghc8.8 does not infer kindRejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```Rejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18910Orderdependent type inference due to Note [Instance and Given overlap]20210106T03:39:21ZRichard Eisenbergrae@richarde.devOrderdependent type inference due to Note [Instance and Given overlap]With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.