GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210226T16:56:43Zhttps://gitlab.haskell.org/ghc/ghc//issues/19432GHC 9.0 rejects default signature that 8.10 accepts20210226T16:56:43ZRyan ScottGHC 9.0 rejects default signature that 8.10 acceptsI originally noticed this issue in the `barbies2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Coerce
import Data.Kind
import Data.Proxy
import GHC.Generics
import GHC.TypeNats
class FunctorT (t :: (k > Type) > k' > Type) where
tmap :: forall f g
. (forall a . f a > g a)
> (forall x . t f x > t g x)
 Default implementation of 'tmap' based on 'Generic'.
default tmap
:: forall f g
. (forall a . f a > g a)
> (forall x. CanDeriveFunctorT t f g x => t f x > t g x)
tmap f = toP (Proxy @1) . gmap (Proxy @1) f . fromP (Proxy @1)
type CanDeriveFunctorT t f g x
= ( GenericP 1 (t f x)
, GenericP 1 (t g x)
, GFunctor 1 f g (RepP 1 (t f x)) (RepP 1 (t g x))
)

class GFunctor (n :: Nat) f g repbf repbg where
gmap :: Proxy n > (forall a . f a > g a) > repbf x > repbg x
class
( Coercible (Rep a) (RepP n a)
, Generic a
) => GenericP (n :: Nat) (a :: Type) where
type family RepP n a :: Type > Type
toP :: Proxy n > RepP n a x > a
fromP :: Proxy n > a > RepP n a x
```
The important bit is the default signature for `tmap`. With GHC 9.0.1, this is rejected thusly:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:24:11: error:
• The default type signature for tmap:
forall (f :: k > *) (g :: k > *).
(forall (a :: k). f a > g a)
> forall (x :: k'). CanDeriveFunctorT t f g x => t f x > t g x
does not match its corresponding nondefault type signature
• When checking the class method:
tmap :: forall k k' (t :: (k > *) > k' > *) (f :: k > *)
(g :: k > *).
FunctorT t =>
(forall (a :: k). f a > g a) > forall (x :: k'). t f x > t g x
In the class declaration for ‘FunctorT’

24  default tmap
 ^^^^
```
Why does GHC 9.0.1 reject this? According to the [GHC User's Guide section on `DefaultSignatures`](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html#defaultmethodsignatures):
> The type signature for a default method of a type class must take on the same form as the corresponding main method’s type signature. Otherwise, the typechecker will reject that class’s definition. By “take on the same form”, we mean that the default type signature should differ from the main type signature only in their contexts.
As far as I can tell, `tmap` meets this criterion, as the only difference between the two signatures is the presence of `CanDeriveFunctorT t f g x =>` in the default signature.I originally noticed this issue in the `barbies2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Coerce
import Data.Kind
import Data.Proxy
import GHC.Generics
import GHC.TypeNats
class FunctorT (t :: (k > Type) > k' > Type) where
tmap :: forall f g
. (forall a . f a > g a)
> (forall x . t f x > t g x)
 Default implementation of 'tmap' based on 'Generic'.
default tmap
:: forall f g
. (forall a . f a > g a)
> (forall x. CanDeriveFunctorT t f g x => t f x > t g x)
tmap f = toP (Proxy @1) . gmap (Proxy @1) f . fromP (Proxy @1)
type CanDeriveFunctorT t f g x
= ( GenericP 1 (t f x)
, GenericP 1 (t g x)
, GFunctor 1 f g (RepP 1 (t f x)) (RepP 1 (t g x))
)

class GFunctor (n :: Nat) f g repbf repbg where
gmap :: Proxy n > (forall a . f a > g a) > repbf x > repbg x
class
( Coercible (Rep a) (RepP n a)
, Generic a
) => GenericP (n :: Nat) (a :: Type) where
type family RepP n a :: Type > Type
toP :: Proxy n > RepP n a x > a
fromP :: Proxy n > a > RepP n a x
```
The important bit is the default signature for `tmap`. With GHC 9.0.1, this is rejected thusly:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:24:11: error:
• The default type signature for tmap:
forall (f :: k > *) (g :: k > *).
(forall (a :: k). f a > g a)
> forall (x :: k'). CanDeriveFunctorT t f g x => t f x > t g x
does not match its corresponding nondefault type signature
• When checking the class method:
tmap :: forall k k' (t :: (k > *) > k' > *) (f :: k > *)
(g :: k > *).
FunctorT t =>
(forall (a :: k). f a > g a) > forall (x :: k'). t f x > t g x
In the class declaration for ‘FunctorT’

24  default tmap
 ^^^^
```
Why does GHC 9.0.1 reject this? According to the [GHC User's Guide section on `DefaultSignatures`](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html#defaultmethodsignatures):
> The type signature for a default method of a type class must take on the same form as the corresponding main method’s type signature. Otherwise, the typechecker will reject that class’s definition. By “take on the same form”, we mean that the default type signature should differ from the main type signature only in their contexts.
As far as I can tell, `tmap` meets this criterion, as the only difference between the two signatures is the presence of `CanDeriveFunctorT t f g x =>` in the default signature.https://gitlab.haskell.org/ghc/ghc//issues/19364oversized source range in type error message20210226T16:40:16Zjwaldmannoversized source range in type error messageFor this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:721: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] [Char]
• In the expression: Pair "yes" "no"
In an equation for ‘baz’: baz = Pair "yes" "no"

7  baz = Pair "yes" "no"
 ^^^^^^^^^^^^^^^
```
So, which argument is wrong?
In fact, how many are?
```
baz :: Pair Foo Bar
baz = Pair "yes" ()
B.hs:7:719: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] ()
• In the expression: Pair "yes" ()
In an equation for ‘baz’: baz = Pair "yes" ()

7  baz = Pair "yes" ()
 ^^^^^^^^^^^^^
```
The following case works better (it shows that the first argument is the problem). What's the difference?
```
foo :: (Foo,Bar)
foo = ("yes", "no")
B.hs:11:812: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Foo
Actual type: [Char]
• In the expression: "yes"
In the expression: ("yes", "no")
In an equation for ‘foo’: foo = ("yes", "no")

11  foo = ("yes", "no")
 ^^^^^
```For this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:721: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] [Char]
• In the expression: Pair "yes" "no"
In an equation for ‘baz’: baz = Pair "yes" "no"

7  baz = Pair "yes" "no"
 ^^^^^^^^^^^^^^^
```
So, which argument is wrong?
In fact, how many are?
```
baz :: Pair Foo Bar
baz = Pair "yes" ()
B.hs:7:719: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] ()
• In the expression: Pair "yes" ()
In an equation for ‘baz’: baz = Pair "yes" ()

7  baz = Pair "yes" ()
 ^^^^^^^^^^^^^
```
The following case works better (it shows that the first argument is the problem). What's the difference?
```
foo :: (Foo,Bar)
foo = ("yes", "no")
B.hs:11:812: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Foo
Actual type: [Char]
• In the expression: "yes"
In the expression: ("yes", "no")
In an equation for ‘foo’: foo = ("yes", "no")

11  foo = ("yes", "no")
 ^^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/19396Surprising lack of generalisation using MonoLocalBinds20210226T03:04:09ZTom EllisSurprising lack of generalisation using MonoLocalBinds## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on HaskellCafe](https://mail.haskell.org/pipermail/haskellcafe/2021February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE ScopedTypeVariables #}
 This code came up in the context of writing a parser, but that's
 not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
 DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
 Does not type check
pFG1 :: Parser B > Parser (D B)
pFG1 pBArg = pBD GF AP <> pBD DF AM
where pBD f p = f p <$> pBArg
 Does type check
pFG2 :: Parser B > Parser (D B)
pFG2 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 Does not type check
pFG3 :: forall b. Parser b > Parser (D b)
pFG3 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 The specifics of the parser don't matter
data Parser a = Parser
(<>) :: Parser a > Parser a > Parser a
(<>) _ _ = Parser
(<$>) :: (a > b) > Parser a > Parser b
(<$>) _ _ = Parser
```## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on HaskellCafe](https://mail.haskell.org/pipermail/haskellcafe/2021February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE ScopedTypeVariables #}
 This code came up in the context of writing a parser, but that's
 not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
 DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
 Does not type check
pFG1 :: Parser B > Parser (D B)
pFG1 pBArg = pBD GF AP <> pBD DF AM
where pBD f p = f p <$> pBArg
 Does type check
pFG2 :: Parser B > Parser (D B)
pFG2 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 Does not type check
pFG3 :: forall b. Parser b > Parser (D b)
pFG3 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 The specifics of the parser don't matter
data Parser a = Parser
(<>) :: Parser a > Parser a > Parser a
(<>) _ _ = Parser
(<$>) :: (a > b) > Parser a > Parser b
(<$>) _ _ = Parser
```https://gitlab.haskell.org/ghc/ghc//issues/19428Deprecate `Winaccessiblecode`20210225T16:15:00ZSebastian GrafDeprecate `Winaccessiblecode`In https://gitlab.haskell.org/ghc/ghc//merge_requests/5100#note_333682, the special role of `Winaccessiblecode` came up. In particular, how it's not integrated well with the rest of how the patternmatch checker works today. For one, it's implemented somewhere in the typechecker, I think. But I also think its purpose is subsumed by `Woverlappingpatterns` (which will warn for *any* inaccessible RHS, not just those caused by contradictory type constraints) noawadays.
I propose to deprecate the flag.In https://gitlab.haskell.org/ghc/ghc//merge_requests/5100#note_333682, the special role of `Winaccessiblecode` came up. In particular, how it's not integrated well with the rest of how the patternmatch checker works today. For one, it's implemented somewhere in the typechecker, I think. But I also think its purpose is subsumed by `Woverlappingpatterns` (which will warn for *any* inaccessible RHS, not just those caused by contradictory type constraints) noawadays.
I propose to deprecate the flag.https://gitlab.haskell.org/ghc/ghc//issues/19419GHC 9.0 unable to deduce that instance signature is at least as general as cl...20210225T03:14:03ZsheafGHC 9.0 unable to deduce that instance signature is at least as general as class signatureThe following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE InstanceSigs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
module Bug where
 base
import Data.Kind
( Constraint )

data SplineType = Open  Closed
data Curve ( clo :: SplineType ) = Curve { ... }
data Spline ( clo :: SplineType ) = Spline { ... }
class KnownSplineType ( clo :: SplineType ) where
type TraversalCt clo ( clo' :: SplineType ) :: Constraint
biwitherSpline
:: ( forall clo'. ( TraversalCt clo clo' )
=> Curve clo' > Maybe ( Curve clo' )
)
> Spline clo
> Maybe ( Spline clo )
instance KnownSplineType Open where
type TraversalCt Open clo' = clo' ~ Open
biwitherSpline
:: ( Curve Open > Maybe ( Curve Open ) )
> Spline Open
> Maybe ( Spline Open )
biwitherSpline _ _ = undefined
```
With GHC 9.0, I get the following error:
```
Bug.hs:37:8: error:
* Couldn't match type: Curve 'Open > Maybe (Curve 'Open)
with: forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo')
Expected: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo'))
> Spline 'Open > Maybe (Spline 'Open)
Actual: (Curve 'Open > Maybe (Curve 'Open))
> Spline 'Open > Maybe (Spline 'Open)
* When checking that instance signature for `biwitherSpline'
is more general than its signature in the class
Instance sig: (Curve 'Open > Maybe (Curve 'Open))
> Spline 'Open > Maybe (Spline 'Open)
Class sig: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo'))
> Spline 'Open > Maybe (Spline 'Open)
In the instance declaration for `KnownSplineType 'Open'

37  :: ( Curve Open > Maybe ( Curve Open ) )
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
It seems that GHC 9.0 is unable to use the associated type family instance `TraversalCt Open clo' = clo' ~ Open` in checking that the instance signature is at least as general as the class signature. Is this expected, or an oversight?
Of course, changing the instance signature to the obviously correct
```haskell
biwitherSpline
:: ( forall clo'. ( TraversalCt Open clo' )
=> Curve clo' > Maybe ( Curve clo' )
)
> Spline Open
> Maybe ( Spline Open )
```
makes the program compile again, but I think the other instance signature should also be accepted.The following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE InstanceSigs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
module Bug where
 base
import Data.Kind
( Constraint )

data SplineType = Open  Closed
data Curve ( clo :: SplineType ) = Curve { ... }
data Spline ( clo :: SplineType ) = Spline { ... }
class KnownSplineType ( clo :: SplineType ) where
type TraversalCt clo ( clo' :: SplineType ) :: Constraint
biwitherSpline
:: ( forall clo'. ( TraversalCt clo clo' )
=> Curve clo' > Maybe ( Curve clo' )
)
> Spline clo
> Maybe ( Spline clo )
instance KnownSplineType Open where
type TraversalCt Open clo' = clo' ~ Open
biwitherSpline
:: ( Curve Open > Maybe ( Curve Open ) )
> Spline Open
> Maybe ( Spline Open )
biwitherSpline _ _ = undefined
```
With GHC 9.0, I get the following error:
```
Bug.hs:37:8: error:
* Couldn't match type: Curve 'Open > Maybe (Curve 'Open)
with: forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo')
Expected: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo'))
> Spline 'Open > Maybe (Spline 'Open)
Actual: (Curve 'Open > Maybe (Curve 'Open))
> Spline 'Open > Maybe (Spline 'Open)
* When checking that instance signature for `biwitherSpline'
is more general than its signature in the class
Instance sig: (Curve 'Open > Maybe (Curve 'Open))
> Spline 'Open > Maybe (Spline 'Open)
Class sig: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' > Maybe (Curve clo'))
> Spline 'Open > Maybe (Spline 'Open)
In the instance declaration for `KnownSplineType 'Open'

37  :: ( Curve Open > Maybe ( Curve Open ) )
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
It seems that GHC 9.0 is unable to use the associated type family instance `TraversalCt Open clo' = clo' ~ Open` in checking that the instance signature is at least as general as the class signature. Is this expected, or an oversight?
Of course, changing the instance signature to the obviously correct
```haskell
biwitherSpline
:: ( forall clo'. ( TraversalCt Open clo' )
=> Curve clo' > Maybe ( Curve clo' )
)
> Spline Open
> Maybe ( Spline Open )
```
makes the program compile again, but I think the other instance signature should also be accepted.https://gitlab.haskell.org/ghc/ghc//issues/1331indexed types panic: wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}20210224T11:23:39ZIan Lynagh <igloo@earth.li>indexed types panic: wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}Lots of indexed types tests are hitting an unhandled case in wrongKindOfFamily, e.g.:
```
Simple1.hs:11:2:ghc6.7.20070504: panic! (the 'impossible' happened)
(GHC version 6.7.20070504 for x86_64unknownlinux):
wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}
```
Affected tests:
```
ATLoop(normal,optc)
GMapAssoc(normal,optc)
GMapTop(normal,optc)
Over(normal)
Records(normal,optc)
Simple1(normal,optc)
Simple10(normal)
Simple11a(normal)
Simple11b(normal)
Simple11c(normal)
Simple11d(normal)
Simple1a(normal)
Simple2(normal,optc)
Simple3(normal,optc)
Simple4(normal,optc)
Simple5(normal,optc)
Simple5a(normal)
Simple5b(normal)
Simple6(normal,optc)
Simple7(normal)
Simple9(normal)
impexp(normal,optc)
ind1(normal,optc)
ind2(normal,optc)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.7 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Unknown 
 Architecture  Unknown 
</details>
<! {"blocked_by":[],"summary":"indexed types panic: wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"6.8 branch","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"Lots of indexed types tests are hitting an unhandled case in wrongKindOfFamily, e.g.:\r\n{{{\r\nSimple1.hs:11:2:ghc6.7.20070504: panic! (the 'impossible' happened)\r\n (GHC version 6.7.20070504 for x86_64unknownlinux):\r\n wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}\r\n}}}\r\nAffected tests:\r\n{{{\r\n ATLoop(normal,optc)\r\n GMapAssoc(normal,optc)\r\n GMapTop(normal,optc)\r\n Over(normal)\r\n Records(normal,optc)\r\n Simple1(normal,optc)\r\n Simple10(normal)\r\n Simple11a(normal)\r\n Simple11b(normal)\r\n Simple11c(normal)\r\n Simple11d(normal)\r\n Simple1a(normal)\r\n Simple2(normal,optc)\r\n Simple3(normal,optc)\r\n Simple4(normal,optc)\r\n Simple5(normal,optc)\r\n Simple5a(normal)\r\n Simple5b(normal)\r\n Simple6(normal,optc)\r\n Simple7(normal)\r\n Simple9(normal)\r\n impexp(normal,optc)\r\n ind1(normal,optc)\r\n ind2(normal,optc)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Lots of indexed types tests are hitting an unhandled case in wrongKindOfFamily, e.g.:
```
Simple1.hs:11:2:ghc6.7.20070504: panic! (the 'impossible' happened)
(GHC version 6.7.20070504 for x86_64unknownlinux):
wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}
```
Affected tests:
```
ATLoop(normal,optc)
GMapAssoc(normal,optc)
GMapTop(normal,optc)
Over(normal)
Records(normal,optc)
Simple1(normal,optc)
Simple10(normal)
Simple11a(normal)
Simple11b(normal)
Simple11c(normal)
Simple11d(normal)
Simple1a(normal)
Simple2(normal,optc)
Simple3(normal,optc)
Simple4(normal,optc)
Simple5(normal,optc)
Simple5a(normal)
Simple5b(normal)
Simple6(normal,optc)
Simple7(normal)
Simple9(normal)
impexp(normal,optc)
ind1(normal,optc)
ind2(normal,optc)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.7 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  Unknown 
 Architecture  Unknown 
</details>
<! {"blocked_by":[],"summary":"indexed types panic: wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"6.8 branch","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"Lots of indexed types tests are hitting an unhandled case in wrongKindOfFamily, e.g.:\r\n{{{\r\nSimple1.hs:11:2:ghc6.7.20070504: panic! (the 'impossible' happened)\r\n (GHC version 6.7.20070504 for x86_64unknownlinux):\r\n wrongKindOfFamily main:ShouldCompile.Sd{tc r6A}\r\n}}}\r\nAffected tests:\r\n{{{\r\n ATLoop(normal,optc)\r\n GMapAssoc(normal,optc)\r\n GMapTop(normal,optc)\r\n Over(normal)\r\n Records(normal,optc)\r\n Simple1(normal,optc)\r\n Simple10(normal)\r\n Simple11a(normal)\r\n Simple11b(normal)\r\n Simple11c(normal)\r\n Simple11d(normal)\r\n Simple1a(normal)\r\n Simple2(normal,optc)\r\n Simple3(normal,optc)\r\n Simple4(normal,optc)\r\n Simple5(normal,optc)\r\n Simple5a(normal)\r\n Simple5b(normal)\r\n Simple6(normal,optc)\r\n Simple7(normal)\r\n Simple9(normal)\r\n impexp(normal,optc)\r\n ind1(normal,optc)\r\n ind2(normal,optc)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >6.8.1https://gitlab.haskell.org/ghc/ghc//issues/8095TypeFamilies painfully slow20210223T14:31:25ZMikeIzbickiTypeFamilies painfully slowI'm using the TypeFamilies extension to generate types that are quite large. GHC can handle these large types fine when they are created manually, but when type families get involved, GHC's performance dies.
Unlike in ticket #5321, using tail recursion does not eliminate the problem, and the order of arguments greatly affects compile time.
I've attached a file Types.hs that demonstrates the problems:
<details><summary>Types.hs</summary>
```haskell
import System.Environment
code :: Int > String > String > String
code i familyTest instanceTest = concat $ map (++"\n") $
[ "{# LANGUAGE TypeOperators,DataKinds,KindSignatures,TypeFamilies,PolyKinds,UndecidableInstances #}"
, "import GHC.TypeLits"
, "data Nat1 = Zero  Succ Nat1"
]
++
case head familyTest of
'a' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 Zero x = '[]"
, "type instance Replicate1 (Succ n) x = x ': (Replicate1 n x)"
]
'b' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 n x = Replicate1' '[] n x "
, "type family Replicate1' (acc::[a]) (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1' acc Zero x = acc"
, "type instance Replicate1' acc (Succ n) x = Replicate1' (x ': acc) n x "
]
'c' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 n x = Replicate1' n x '[]"
, "type family Replicate1' (n :: Nat1) (x::a) (acc::[a]) :: [a]"
, "type instance Replicate1' Zero x acc = acc"
, "type instance Replicate1' (Succ n) x acc = Replicate1' n x (x ': acc)"
]
++
[ "class Class a where"
, " f :: a > a"
, "data Data (xs::a) = X  Y"
, " deriving (Read,Show)"
, "main = print test1"
]
++
case head instanceTest of
'a' >
[ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
]
'b' >
[ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
]
'c' >
[ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( ("++mkList i++") ))"
]
'd' >
[ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( ("++mkList i++") ))"
]
mkList :: Int > String
mkList 0 = " '[] "
mkList i = " () ': " ++ mkList (i1)
mkNat1 :: Int > String
mkNat1 0 = " Zero "
mkNat1 i = " Succ ( " ++ mkNat1 (i1) ++ ")"
main = do
numstr : familyTest : instanceTest : xs < getArgs
let num = read numstr :: Int
putStrLn $ code num familyTest instanceTest
```
</details>
This file generates another Haskell file which has the problems. It takes 3 flags. The first is the size of the type to generate, the second is which type family function to use, and the third is whether to call the type family or just use a manually generated type.
Here are my performance results:
Using nontail recursion, I get these results. I have to increase the stack size based on the size of the type I want to generate.
```
$ ./Types 200 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m2.973s
$ ./Types 300 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=350
real 0m6.018s
$ ./Types 400 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=450
real 0m9.995s
$ ./Types 500 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=550
real 0m15.645s
```
Tail recursion generates much slower compile times for some reason, and I still need to adjust the stack size:
```
$ ./Types 200 b a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m16.120s
```
Changing the order of arguments to the recursive type family greatly changes the run times:
```
$ ./Types 200 c a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m6.095s
```
Without the type family, I get MUCH better performance:
```
$ ./Types 10000 a d > test.hs && time ghc test.hs > /dev/null
real 0m2.271s
```
See also: #17223
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #5321 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeFamilies painfully slow","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[5321],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm using the TypeFamilies extension to generate types that are quite large. GHC can handle these large types fine when they are created manually, but when type families get involved, GHC's performance dies.\r\n\r\nUnlike in ticket #5321, using tail recursion does not eliminate the problem, and the order of arguments greatly affects compile time.\r\n\r\nI've attached a file Types.hs that demonstrates the problems. This file generates another Haskell file which has the problems. It takes 3 flags. The first is the size of the type to generate, the second is which type family function to use, and the third is whether to call the type family or just use a manually generated type.\r\n\r\nHere are my performance results:\r\n\r\nUsing nontail recursion, I get these results. I have to increase the stack size based on the size of the type I want to generate.\r\n\r\n{{{\r\n$ ./Types 200 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m2.973s\r\n$ ./Types 300 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=350\r\nreal 0m6.018s\r\n$ ./Types 400 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=450\r\nreal 0m9.995s\r\n$ ./Types 500 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=550\r\nreal 0m15.645s\r\n}}}\r\nTail recursion generates much slower compile times for some reason, and I still need to adjust the stack size:\r\n{{{\r\n$ ./Types 200 b a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m16.120s\r\n}}}\r\nChanging the order of arguments to the recursive type family greatly changes the run times:\r\n{{{\r\n$ ./Types 200 c a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m6.095s\r\n}}}\r\nWithout the type family, I get MUCH better performance:\r\n{{{\r\n$ ./Types 10000 a d > test.hs && time ghc test.hs > /dev/null\r\nreal 0m2.271s\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I'm using the TypeFamilies extension to generate types that are quite large. GHC can handle these large types fine when they are created manually, but when type families get involved, GHC's performance dies.
Unlike in ticket #5321, using tail recursion does not eliminate the problem, and the order of arguments greatly affects compile time.
I've attached a file Types.hs that demonstrates the problems:
<details><summary>Types.hs</summary>
```haskell
import System.Environment
code :: Int > String > String > String
code i familyTest instanceTest = concat $ map (++"\n") $
[ "{# LANGUAGE TypeOperators,DataKinds,KindSignatures,TypeFamilies,PolyKinds,UndecidableInstances #}"
, "import GHC.TypeLits"
, "data Nat1 = Zero  Succ Nat1"
]
++
case head familyTest of
'a' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 Zero x = '[]"
, "type instance Replicate1 (Succ n) x = x ': (Replicate1 n x)"
]
'b' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 n x = Replicate1' '[] n x "
, "type family Replicate1' (acc::[a]) (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1' acc Zero x = acc"
, "type instance Replicate1' acc (Succ n) x = Replicate1' (x ': acc) n x "
]
'c' >
[ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
, "type instance Replicate1 n x = Replicate1' n x '[]"
, "type family Replicate1' (n :: Nat1) (x::a) (acc::[a]) :: [a]"
, "type instance Replicate1' Zero x acc = acc"
, "type instance Replicate1' (Succ n) x acc = Replicate1' n x (x ': acc)"
]
++
[ "class Class a where"
, " f :: a > a"
, "data Data (xs::a) = X  Y"
, " deriving (Read,Show)"
, "main = print test1"
]
++
case head instanceTest of
'a' >
[ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
]
'b' >
[ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
]
'c' >
[ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( ("++mkList i++") ))"
]
'd' >
[ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
, " f X = Y"
, " f Y = X"
, "test1 = f (X :: Data ( ("++mkList i++") ))"
]
mkList :: Int > String
mkList 0 = " '[] "
mkList i = " () ': " ++ mkList (i1)
mkNat1 :: Int > String
mkNat1 0 = " Zero "
mkNat1 i = " Succ ( " ++ mkNat1 (i1) ++ ")"
main = do
numstr : familyTest : instanceTest : xs < getArgs
let num = read numstr :: Int
putStrLn $ code num familyTest instanceTest
```
</details>
This file generates another Haskell file which has the problems. It takes 3 flags. The first is the size of the type to generate, the second is which type family function to use, and the third is whether to call the type family or just use a manually generated type.
Here are my performance results:
Using nontail recursion, I get these results. I have to increase the stack size based on the size of the type I want to generate.
```
$ ./Types 200 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m2.973s
$ ./Types 300 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=350
real 0m6.018s
$ ./Types 400 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=450
real 0m9.995s
$ ./Types 500 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=550
real 0m15.645s
```
Tail recursion generates much slower compile times for some reason, and I still need to adjust the stack size:
```
$ ./Types 200 b a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m16.120s
```
Changing the order of arguments to the recursive type family greatly changes the run times:
```
$ ./Types 200 c a > test.hs && time ghc test.hs > /dev/null fcontextstack=250
real 0m6.095s
```
Without the type family, I get MUCH better performance:
```
$ ./Types 10000 a d > test.hs && time ghc test.hs > /dev/null
real 0m2.271s
```
See also: #17223
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.6.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #5321 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeFamilies painfully slow","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[5321],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm using the TypeFamilies extension to generate types that are quite large. GHC can handle these large types fine when they are created manually, but when type families get involved, GHC's performance dies.\r\n\r\nUnlike in ticket #5321, using tail recursion does not eliminate the problem, and the order of arguments greatly affects compile time.\r\n\r\nI've attached a file Types.hs that demonstrates the problems. This file generates another Haskell file which has the problems. It takes 3 flags. The first is the size of the type to generate, the second is which type family function to use, and the third is whether to call the type family or just use a manually generated type.\r\n\r\nHere are my performance results:\r\n\r\nUsing nontail recursion, I get these results. I have to increase the stack size based on the size of the type I want to generate.\r\n\r\n{{{\r\n$ ./Types 200 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m2.973s\r\n$ ./Types 300 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=350\r\nreal 0m6.018s\r\n$ ./Types 400 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=450\r\nreal 0m9.995s\r\n$ ./Types 500 a a > test.hs && time ghc test.hs > /dev/null fcontextstack=550\r\nreal 0m15.645s\r\n}}}\r\nTail recursion generates much slower compile times for some reason, and I still need to adjust the stack size:\r\n{{{\r\n$ ./Types 200 b a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m16.120s\r\n}}}\r\nChanging the order of arguments to the recursive type family greatly changes the run times:\r\n{{{\r\n$ ./Types 200 c a > test.hs && time ghc test.hs > /dev/null fcontextstack=250\r\nreal 0m6.095s\r\n}}}\r\nWithout the type family, I get MUCH better performance:\r\n{{{\r\n$ ./Types 10000 a d > test.hs && time ghc test.hs > /dev/null\r\nreal 0m2.271s\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.4.1Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc//issues/14422{# complete #} should be able to be at least partially type directed20210222T22:36:24ZEdward Kmett{# complete #} should be able to be at least partially type directedThe fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 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":"{# complete #} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{# complete #}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{# complete (:<), Empty #}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `Wnoincompletepatterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/19154GHC 9.0 no longer typechecks a program involving overloaded labels and type a...20210222T09:40:05ZsheafGHC 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 )
```9.2.1https://gitlab.haskell.org/ghc/ghc//issues/19167Regression around overloaded literals and type applications20210221T16:41:22ZRichard 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.x9.2.1https://gitlab.haskell.org/ghc/ghc//issues/17934Consider using specificity to disambiguate quantified constraints20210221T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show`  maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a > String` is the default method implementation for `show`. When typechecking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the toplevel instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instancelookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (nonquantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1`  just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be nonquantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a nonquantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be setlike, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc//issues/8392Suggest AllowAmbiguousTypes20210219T17:55:49ZrwbartonSuggest 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)
bound by an instance declaration:
(Fun f b c, Fun g a b) => Fun (Compose f g) a c
at tf.hs:38:1056
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:1056\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":[]} >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:1056
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:1056\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/18738Infer multiplicity of case expression20210218T10:48:10ZArnaud SpiwackInfer multiplicity of case expression## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidal## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidalhttps://gitlab.haskell.org/ghc/ghc//issues/19131Does the subtype check in Note [Impedance matching] ever fail?20210217T13:00:27ZRichard 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/17333Coercible solver does not look through "class newtypes"20210216T21:35:31ZRyan ScottCoercible solver does not look through "class newtypes"The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.The code below makes use of the "class newtype" design pattern:
```hs
class Show a => MyShow a
instance Show a => MyShow a
```
`MyShow` is a newtype around `Show` in the sense that when compiled to Core, a `MyShow` dictionary is literally a newtype around `Show`. Unfortunately, this newtype treatment does not extend to the `Coercible` solver, as the following example demonstrates:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Bug where
import Data.Coerce
class Show a => MyShow a
instance Show a => MyShow a
newtype T1 a = MkT1 ( Show a => a > a > String)
newtype T2 a = MkT2 (MyShow a => a > a > String)
f :: T1 a > T2 a
f = coerce
```
```
$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:5: error:
• Couldn't match representation of type ‘MyShow a’
with that of ‘Show a’
arising from a use of ‘coerce’
The data constructor ‘Bug.C:MyShow’
of newtype ‘MyShow’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: T1 a > T2 a (bound at Bug.hs:20:1)

20  f = coerce
 ^^^^^^
```
Somewhat surprisingly, this does not work. Even the error message indicates that `MyShow` is a newtype (which is a bit odd, but whatever), but since the internal `C:MyShow` constructor is not exposed, the `Coercible` solver doesn't have enough information to proceed.
If the following change is applied to GHC, then it typechecks:
```diff
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
 a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ 41,7 +41,7 @@ import Name
import Pair
import Panic
import VarSet
import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
import Control.Monad
#include "HsVersions.h"
@@ 577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= mapStepResult (\co > (unitBag gre, co)) $
unwrapNewTypeStepper rec_nts tc tys
+  isClassTyCon tc && isNewTyCon tc
+ = mapStepResult (\co > (emptyBag, co)) $
+ unwrapNewTypeStepper rec_nts tc tys
+
 otherwise
= NS_Done
```
The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by [Generic Programming of All Kinds](https://victorcmiraldo.github.io/data/hask2018_draft.pdf)):
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module GOAK where
import Data.Coerce
import Data.Kind
newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0
f :: T > TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
@(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
x)

infixr 5 :&&:
data LoT :: Type > Type where
LoT0 :: LoT Type
(:&&:) :: k > LoT ks > LoT (k > ks)
type family HeadLoT (tys :: LoT (k > k')) :: k where
HeadLoT (a :&&: _) = a
type family TailLoT (tys :: LoT (k > k')) :: LoT k' where
TailLoT (_ :&&: as) = as
data TyVar :: Type > Type > Type where
VZ :: TyVar (x > xs) x
VS :: TyVar xs k > TyVar (x > xs) k
data Atom :: Type > Type > Type where
Var :: TyVar d k > Atom d k
Kon :: k > Atom d k
(:@:) :: Atom d (k1 > k2) > Atom d k1 > Atom d k2
(:=>>:) :: Atom d Constraint > Atom d Type > Atom d Type
ForAllQ :: Atom (d1 > d) Constraint > Atom d Constraint
type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
InterpretVar 'VZ tys = HeadLoT tys
InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Interpret ('Var v) tys = InterpretVar v tys
Interpret ('Kon t) tys = t
Interpret (f ':@: x) tys = (Interpret f tys) (Interpret x tys)
Interpret (c ':=>>: f) tys = SuchThatI c f tys
Interpret (ForAllQ f) tys = ForAllQI f tys
newtype SuchThatI :: Atom d Constraint > Atom d Type > LoT d > Type where
SuchThatI :: (Interpret c tys => Interpret f tys) > SuchThatI c f tys
class (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 > d) Constraint) (tys :: LoT d)
class Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
newtype Field :: Atom d Type > LoT d > Type where
Field :: { unField :: Interpret t x } > Field t x
```
`f` will not typecheck without the ability to coerce from `ForAllQI f tys` to `forall t. WrappedQI f (t ':&&: tys)`. Moreover, it would be extremely difficult to write `f` _without_ `coerce`.https://gitlab.haskell.org/ghc/ghc//issues/13655Spurious untouchable type variable in connection with rank2 type and constra...20210215T03:51:51ZWolfgang JeltschSpurious untouchable type variable in connection with rank2 type and constraint familyThe following code cannot be compiled:
```hs
{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) > a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:637
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) > a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) > a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 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":"Spurious untouchable type variable in connection with rank2 type and constraint family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code cannot be compiled:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) > a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:637\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) > a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) > a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following code cannot be compiled:
```hs
{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) > a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:637
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) > a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) > a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1rc2 
 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":"Spurious untouchable type variable in connection with rank2 type and constraint family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code cannot be compiled:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) > a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:637\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) > a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) > a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/19042Regression: HEAD incurs a reduction stack overflow on program involving type ...20210210T21:11:55ZRyan 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/19315GHC 9.0 regression: plots0.1.1.2 fails to build due to ambiguous type variable20210210T21:11:55ZRyan ScottGHC 9.0 regression: plots0.1.1.2 fails to build due to ambiguous type variable_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/568397#L5617)_.
The `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained example with no external dependencies:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a > f b) > s > f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a > f b) > s > f t
type Getting r s a = (a > Const r a) > s > Const r s
type ASetter s t a b = (a > Identity b) > s > Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n > V2 n
flipX_Y (V2 x y) = V2 (y) (x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a > (a > b) > b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b > (a > b) > s > t
(%~) = over
(^.) :: s > Getting a s a > a
s ^. l = getConst (l Const s)
over :: ASetter s t a b > (a > b) > s > t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a > m a
view l = asks (getConst . l Const)
lens :: (s > a) > (s > b > t) > Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * > *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * > *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) > a > a
type TextFunction b v n = TextAlignment n > String > QDiagram b v n Any
data TickLabels b (v :: * > *) n = TickLabels
{ tlFun :: [n] > (n,n) > [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b  a > b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f > tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] > (N a, N a) > [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f > tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty > tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n > tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * > *) n = MajorTicks
{ matFunction :: (n,n) > [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) > [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a > mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * > *) n = Path
data (::) u v = (u > v) :: (v > u)
infixr 7 ::
instance Semigroup (a :: a) where
(f :: f') <> (g :: g') = f . g :: g' . f'
instance Monoid (v :: v) where
mempty = id :: id
data Transformation v n = Transformation (v n :: v n) (v n :: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) > t > t
translation :: v n > Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t > t > t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o > a > a > a
orient o h v =
case view orientation o of
Horizontal > h
Vertical > v
data Orientation = Horizontal  Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a > c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * > *) n m = QD
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m  (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText  BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a > p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
> ColourMap
> (n,n)
> n
> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a > a > a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x  (ub + lb)/2) / (ub  lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) > QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) ( w/2  view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc9.0`:
```
$ ~/Software/ghc9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] > (n, n) > [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
> ColourMap > (n, n) > n > QDiagram b V2 n Any
at Bug.hs:(204,1)(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n > Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
 Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds

229  tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
 ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghcbignum backend (fix #18912)`)_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/568397#L5617)_.
The `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained example with no external dependencies:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE RecordWildCards #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a > f b) > s > f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a > f b) > s > f t
type Getting r s a = (a > Const r a) > s > Const r s
type ASetter s t a b = (a > Identity b) > s > Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n > V2 n
flipX_Y (V2 x y) = V2 (y) (x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a > (a > b) > b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b > (a > b) > s > t
(%~) = over
(^.) :: s > Getting a s a > a
s ^. l = getConst (l Const s)
over :: ASetter s t a b > (a > b) > s > t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a > m a
view l = asks (getConst . l Const)
lens :: (s > a) > (s > b > t) > Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * > *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * > *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) > a > a
type TextFunction b v n = TextAlignment n > String > QDiagram b v n Any
data TickLabels b (v :: * > *) n = TickLabels
{ tlFun :: [n] > (n,n) > [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b  a > b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f > tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] > (N a, N a) > [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f > tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty > tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n > tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * > *) n = MajorTicks
{ matFunction :: (n,n) > [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) > [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a > mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * > *) n = Path
data (::) u v = (u > v) :: (v > u)
infixr 7 ::
instance Semigroup (a :: a) where
(f :: f') <> (g :: g') = f . g :: g' . f'
instance Monoid (v :: v) where
mempty = id :: id
data Transformation v n = Transformation (v n :: v n) (v n :: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) > t > t
translation :: v n > Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t > t > t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o > a > a > a
orient o h v =
case view orientation o of
Horizontal > h
Vertical > v
data Orientation = Horizontal  Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a > c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * > *) n m = QD
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m  (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m  (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText  BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a > p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
> ColourMap
> (n,n)
> n
> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a > a > a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x  (ub + lb)/2) / (ub  lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) > QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) ( w/2  view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc9.0`:
```
$ ~/Software/ghc9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] > (n, n) > [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
> ColourMap > (n, n) > n > QDiagram b V2 n Any
at Bug.hs:(204,1)(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n > Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
 Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds

229  tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
 ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghcbignum backend (fix #18912)`)9.0.2https://gitlab.haskell.org/ghc/ghc//issues/19272EGraphs for representation of normalised refinement types in the patternmat...20210129T23:14:50ZSebastian GrafEGraphs for representation of normalised refinement types in the patternmatch checkerI realised today that the quite complicated data structure+invariants (`Nabla`'s [`TmState`](https://gitlab.haskell.org/ghc/ghc//blob/0249974e7622e35927060da21f9231cb1e6357b9/compiler/GHC/HsToCore/Pmc/Solver/Types.hs#L125142)) we use while patternmatch coverage checking fits "egraphs" quite well.
I realised so while reading the POPL 2021 paper [*`egg`: Fast and Extensible Equality Saturation*](https://arxiv.org/abs/2004.03082). The similarity is striking. I think the inhabitation test could probably be expressed as an egraph analysis.
To be a bit more concrete, an egraph is basically a unionfind data structure on terms. If we start with the disjoint equality classes `{Just x}, {Just y}, {x}, {y}` and later find out that `x ~ y`, we'd `merge` the equality classes `{x}` and `{y}`. The egraph data structure then restores congruence, putting `Just x` and `Just y` into the same equality class as well: `{Just x, Just y}, {x, y}`. Note how this also puts the "CSE" pass envisioned in #17208 on firm ground. There we have
```hs
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```
To see that the match is exhaustive, we have to see that `reverse xs ~ reverse xs'` from `xs ~ xs'`. This is exactly the kind of congruence that egraphs maintain: Replace `Just` by `reverse` in the example above. (It does so via a technique called "upward merge" that we'd have to implement in an adhoc manner to fix #17208).
The egraph representation is quite compact and trivially supports the ∆(x) lookup from the paper (it's just the `find` operation), and extends it to expressions, ∆(e), via `canonicalize`.
While I think this is an important and useful observation, I'm not so keen about implementing it; it's a bit unclear to me if we can retain the same (mostly sufficient) efficiency that our checker has today, and #17208 alone is not compelling enough of a use case for me to pursue.
Maybe that data structure would be useful in other parts of GHC as well. I imagine that Type Family rewrites fit into the same framework. It was conceived for theorem provers, after all. Maybe it's also a useful representation for the Simplifier, although implementing it would be a huge change with possibly daunting repercussions. Still, a good data structure to have up one's sleeve.I realised today that the quite complicated data structure+invariants (`Nabla`'s [`TmState`](https://gitlab.haskell.org/ghc/ghc//blob/0249974e7622e35927060da21f9231cb1e6357b9/compiler/GHC/HsToCore/Pmc/Solver/Types.hs#L125142)) we use while patternmatch coverage checking fits "egraphs" quite well.
I realised so while reading the POPL 2021 paper [*`egg`: Fast and Extensible Equality Saturation*](https://arxiv.org/abs/2004.03082). The similarity is striking. I think the inhabitation test could probably be expressed as an egraph analysis.
To be a bit more concrete, an egraph is basically a unionfind data structure on terms. If we start with the disjoint equality classes `{Just x}, {Just y}, {x}, {y}` and later find out that `x ~ y`, we'd `merge` the equality classes `{x}` and `{y}`. The egraph data structure then restores congruence, putting `Just x` and `Just y` into the same equality class as well: `{Just x, Just y}, {x, y}`. Note how this also puts the "CSE" pass envisioned in #17208 on firm ground. There we have
```hs
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```
To see that the match is exhaustive, we have to see that `reverse xs ~ reverse xs'` from `xs ~ xs'`. This is exactly the kind of congruence that egraphs maintain: Replace `Just` by `reverse` in the example above. (It does so via a technique called "upward merge" that we'd have to implement in an adhoc manner to fix #17208).
The egraph representation is quite compact and trivially supports the ∆(x) lookup from the paper (it's just the `find` operation), and extends it to expressions, ∆(e), via `canonicalize`.
While I think this is an important and useful observation, I'm not so keen about implementing it; it's a bit unclear to me if we can retain the same (mostly sufficient) efficiency that our checker has today, and #17208 alone is not compelling enough of a use case for me to pursue.
Maybe that data structure would be useful in other parts of GHC as well. I imagine that Type Family rewrites fit into the same framework. It was conceived for theorem provers, after all. Maybe it's also a useful representation for the Simplifier, although implementing it would be a huge change with possibly daunting repercussions. Still, a good data structure to have up one's sleeve.https://gitlab.haskell.org/ghc/ghc//issues/12088Type/data family instances in kind checking20210125T22:43:11ZalexviethType/data family instances in kind checkingIn `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note
```hs
data family T a
data instance T Int = MkT
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
ddumprntrace shows these groups
```
rnTycl dependency analysis made groups
[[data family T a_apG]
[]
[data instance T Int = MkT],
[data Proxy (a_apF :: k_apE)]
[]
[],
[data S = MkS (Proxy MkT)]
[]
[]]
```
That's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.
See also
* #11348
* #16693
* #16410
* #19527
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #11348 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Promote data family instance constructors","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[11348],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note\r\n\r\n{{{#!hs\r\ndata family T a\r\ndata instance T Int = MkT\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\nddumprntrace shows these groups\r\n\r\n{{{\r\nrnTycl dependency analysis made groups\r\n [[data family T a_apG]\r\n []\r\n [data instance T Int = MkT],\r\n [data Proxy (a_apF :: k_apE)]\r\n []\r\n [],\r\n [data S = MkS (Proxy MkT)]\r\n []\r\n []]\r\n}}}\r\n\r\nThat's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.","type_of_failure":"OtherFailure","blocking":[]} >In `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note
```hs
data family T a
data instance T Int = MkT
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
ddumprntrace shows these groups
```
rnTycl dependency analysis made groups
[[data family T a_apG]
[]
[data instance T Int = MkT],
[data Proxy (a_apF :: k_apE)]
[]
[],
[data S = MkS (Proxy MkT)]
[]
[]]
```
That's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.
See also
* #11348
* #16693
* #16410
* #19527
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #11348 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Promote data family instance constructors","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[11348],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In `TcEnv.hs` there is a note AFamDataCon: not promoting data family constructors. It states that we can't use a promoted data family instance constructor because we would have to interleave the checking of instances and data types. But with the fix of #11348, we now do exactly this. In the example from the note\r\n\r\n{{{#!hs\r\ndata family T a\r\ndata instance T Int = MkT\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\nddumprntrace shows these groups\r\n\r\n{{{\r\nrnTycl dependency analysis made groups\r\n [[data family T a_apG]\r\n []\r\n [data instance T Int = MkT],\r\n [data Proxy (a_apF :: k_apE)]\r\n []\r\n [],\r\n [data S = MkS (Proxy MkT)]\r\n []\r\n []]\r\n}}}\r\n\r\nThat's to say, the instance `T Int` will in fact be checked before `S`. So let's remove this restriction.","type_of_failure":"OtherFailure","blocking":[]} >9.2.1Vladislav ZavialovArtyom KuznetsovVladislav Zavialov