GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201027T19:18:51Zhttps://gitlab.haskell.org/ghc/ghc//issues/18855GHC 9.0+ regression in checking program with higherrank kinds20201027T19:18:51ZRyan ScottGHC 9.0+ regression in checking program with higherrank kindsGHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```GHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```9.0.1https://gitlab.haskell.org/ghc/ghc//issues/18759Types with different forall placements don't unify with QL ImpredicativeTypes20201029T09:14:09ZAndrzej RybczakTypes with different forall placements don't unify with QL ImpredicativeTypesThe following program:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# OPTIONS_GHC Wall #}
import GHC.TypeLits
main :: IO ()
main = pure ()
data X = X { x :: forall a. a > a }
class HasField (name :: Symbol) s a  name s > a where
getField :: s > a
instance a ~ (forall x. x > x) => HasField "x" X a where
getField = x
getX_Ok_sel :: X > forall a. a > a
getX_Ok_sel = x
getX_Bad_sel :: forall a. X > a > a
getX_Bad_sel = x
getX_Ok_class :: X > forall a. a > a
getX_Ok_class = getField @"x"
getX_Bad_class :: forall a. X > a > a
getX_Bad_class = getField @"x"
getX_Bad_classUsage :: String
getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
produces errors with GHC 9.1.0.20200927:
```
unknown@electronics _build $ ./ghcstage1 it.hs
[1 of 1] Compiling Main ( it.hs, it.o )
it.hs:29:16: error:
• Couldn't match type: forall a1. a1 > a1
with: a > a
Expected: X > a > a
Actual: X > forall a. a > a
• In the expression: x
In an equation for ‘getX_Bad_sel’: getX_Bad_sel = x
• Relevant bindings include
getX_Bad_sel :: X > a > a (bound at it.hs:29:1)

29  getX_Bad_sel = x
 ^
it.hs:35:18: error:
• Couldn't match type: a > a
with: forall x. x > x
arising from a use of ‘getField’
• In the expression: getField @"x"
In an equation for ‘getX_Bad_class’: getX_Bad_class = getField @"x"
• Relevant bindings include
getX_Bad_class :: X > a > a (bound at it.hs:35:1)

35  getX_Bad_class = getField @"x"
 ^^^^^^^^
it.hs:38:23: error:
• Couldn't match type: String > String
with: forall x. x > x
arising from a use of ‘getField’
• In the expression: getField @"x" (X id) "hello world"
In an equation for ‘getX_Bad_classUsage’:
getX_Bad_classUsage = getField @"x" (X id) "hello world"

38  getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
The `Bad_sel` and `Bad_class` issues look very similar, but produce error messages with flipped actual and expected types, which confuses me a bit.
`Bad_classUsage` looks like a consequence of `Bad_class` not working.The following program:
```haskell
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# OPTIONS_GHC Wall #}
import GHC.TypeLits
main :: IO ()
main = pure ()
data X = X { x :: forall a. a > a }
class HasField (name :: Symbol) s a  name s > a where
getField :: s > a
instance a ~ (forall x. x > x) => HasField "x" X a where
getField = x
getX_Ok_sel :: X > forall a. a > a
getX_Ok_sel = x
getX_Bad_sel :: forall a. X > a > a
getX_Bad_sel = x
getX_Ok_class :: X > forall a. a > a
getX_Ok_class = getField @"x"
getX_Bad_class :: forall a. X > a > a
getX_Bad_class = getField @"x"
getX_Bad_classUsage :: String
getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
produces errors with GHC 9.1.0.20200927:
```
unknown@electronics _build $ ./ghcstage1 it.hs
[1 of 1] Compiling Main ( it.hs, it.o )
it.hs:29:16: error:
• Couldn't match type: forall a1. a1 > a1
with: a > a
Expected: X > a > a
Actual: X > forall a. a > a
• In the expression: x
In an equation for ‘getX_Bad_sel’: getX_Bad_sel = x
• Relevant bindings include
getX_Bad_sel :: X > a > a (bound at it.hs:29:1)

29  getX_Bad_sel = x
 ^
it.hs:35:18: error:
• Couldn't match type: a > a
with: forall x. x > x
arising from a use of ‘getField’
• In the expression: getField @"x"
In an equation for ‘getX_Bad_class’: getX_Bad_class = getField @"x"
• Relevant bindings include
getX_Bad_class :: X > a > a (bound at it.hs:35:1)

35  getX_Bad_class = getField @"x"
 ^^^^^^^^
it.hs:38:23: error:
• Couldn't match type: String > String
with: forall x. x > x
arising from a use of ‘getField’
• In the expression: getField @"x" (X id) "hello world"
In an equation for ‘getX_Bad_classUsage’:
getX_Bad_classUsage = getField @"x" (X id) "hello world"

38  getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
The `Bad_sel` and `Bad_class` issues look very similar, but produce error messages with flipped actual and expected types, which confuses me a bit.
`Bad_classUsage` looks like a consequence of `Bad_class` not working.https://gitlab.haskell.org/ghc/ghc//issues/18531Untouchable variable in unused let binding20200930T21:32:15ZMatt NoonanUntouchable variable in unused let binding## Summary
When using GADTs, we observed a surprising "untouchable type variable" error on innocuousseeming code involving
pattern matching on the GADT's sole constructor in a let binding. It may be that everything is operating as designed, but the scenario seemed fragile enough and surprising enough to warrant a report.
## Steps to reproduce
The following code exhibits the issue:
```
{# language GADTs #}
module Untouchable where
data T a where
MkT :: Bool > T Bool
fine :: T a > Int
fine x = let MkT y = x in if y then 1 else 2
sure :: T Bool > Int
sure x = let MkT y = x in 3
nope :: T a > Int
nope x = let MkT y = x in 3
```
`fine` and `sure` compile with no issues, but `nope` causes an error:
```
• Couldn't match expected type ‘p0’ with actual type ‘Bool’
‘p0’ is untouchable
inside the constraints: a ~ Bool
bound by a pattern with constructor: MkT :: Bool > T Bool,
in a pattern binding
at src/Main.hs:14:1418
• In the pattern: MkT y
In a pattern binding: MkT y = x
In the expression: let MkT y = x in 3
```
## Expected behavior
We expected that either `nope` would compile, or else `sure` would fail to compile.
## Environment
* GHC version used:
8.8.3, 8.6.5## Summary
When using GADTs, we observed a surprising "untouchable type variable" error on innocuousseeming code involving
pattern matching on the GADT's sole constructor in a let binding. It may be that everything is operating as designed, but the scenario seemed fragile enough and surprising enough to warrant a report.
## Steps to reproduce
The following code exhibits the issue:
```
{# language GADTs #}
module Untouchable where
data T a where
MkT :: Bool > T Bool
fine :: T a > Int
fine x = let MkT y = x in if y then 1 else 2
sure :: T Bool > Int
sure x = let MkT y = x in 3
nope :: T a > Int
nope x = let MkT y = x in 3
```
`fine` and `sure` compile with no issues, but `nope` causes an error:
```
• Couldn't match expected type ‘p0’ with actual type ‘Bool’
‘p0’ is untouchable
inside the constraints: a ~ Bool
bound by a pattern with constructor: MkT :: Bool > T Bool,
in a pattern binding
at src/Main.hs:14:1418
• In the pattern: MkT y
In a pattern binding: MkT y = x
In the expression: let MkT y = x in 3
```
## Expected behavior
We expected that either `nope` would compile, or else `sure` would fail to compile.
## Environment
* GHC version used:
8.8.3, 8.6.5https://gitlab.haskell.org/ghc/ghc//issues/18529GHC fails to infer type with FlexibleContexts20200930T21:32:01ZRichard Eisenbergrae@richarde.devGHC fails to infer type with FlexibleContextsIf I say
```hs
{# LANGUAGE MultiParamTypeClasses, FlexibleContexts #}
module Bug where
class C a b where
op :: a > b > ()
 foo :: (C a Integer) => a > ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the type of `foo` is ambiguous, because it tries to produce `C a b => a > ()` as the type of `foo`. Instead, it shouldn't quantify `b`, letting it default to `Integer`.
The solution is to use `oclose` instead of `growThetaTyVars` in `decideQuantifiedTyVars`. This will respect functional dependencies, quantifying over `b` only when a fundep exists from `a` to `b`.
I will fix in ongoing work (in the `wip/derivedrefactor` branch).If I say
```hs
{# LANGUAGE MultiParamTypeClasses, FlexibleContexts #}
module Bug where
class C a b where
op :: a > b > ()
 foo :: (C a Integer) => a > ()
foo x = op x 3
```
then GHC complains that the variable `b0` in the type of `foo` is ambiguous, because it tries to produce `C a b => a > ()` as the type of `foo`. Instead, it shouldn't quantify `b`, letting it default to `Integer`.
The solution is to use `oclose` instead of `growThetaTyVars` in `decideQuantifiedTyVars`. This will respect functional dependencies, quantifying over `b` only when a fundep exists from `a` to `b`.
I will fix in ongoing work (in the `wip/derivedrefactor` branch).Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/18102TemplateHaskellQuotes and RebindableSyntax don't play nicely20200805T16:54:27ZRichard Eisenbergrae@richarde.devTemplateHaskellQuotes and RebindableSyntax don't play nicelyEDIT: The original problem described here was about untyped TH, and it was fixed in !2960. But we identify a new problem with typed Template Haskell, which has yet to be solved. https://gitlab.haskell.org/ghc/ghc//issues/18102#note_292247 shows two illustrative examples.

If I say
```hs
{# LANGUAGE TemplateHaskell, RebindableSyntax #}
module Bug where
import Prelude ( Monad(..), Bool(..), print, ($) )
import Language.Haskell.TH.Syntax
$( do stuff < [ if True then 10 else 15 ]
runIO $ print stuff
return [] )
```
then I get errors about `ifThenElse` and `fromInteger` not being in scope. When I bring them into scope, the code is accepted, but the quoted syntax does not mention them, instead accurately reflecting the original source Haskell I wrote.
There are several problems in this story:
1. Template Haskell quotes are meant to work even in the presence of unbound identifiers.
2. Template Haskell is all about quoting (and splicing) surface syntax. Quoting should not care about `XRebindableSyntax`.
3. If we were to decide that quoting should respect `XRebindableSyntax` (I disagree with this design, to be clear), then the output of the quote is incorrect.
I propose: disable `XRebindableSyntax` within quotes. That should fix all these problems.
Other reasonable possibility: disable `XRebindableSyntax` within quotes, but use the TH combinators that are in scope (like `conE` and `appE`, etc.). I think this would be nightmarish to implement, and no one is asking for it, but it would be a consistent way forward.EDIT: The original problem described here was about untyped TH, and it was fixed in !2960. But we identify a new problem with typed Template Haskell, which has yet to be solved. https://gitlab.haskell.org/ghc/ghc//issues/18102#note_292247 shows two illustrative examples.

If I say
```hs
{# LANGUAGE TemplateHaskell, RebindableSyntax #}
module Bug where
import Prelude ( Monad(..), Bool(..), print, ($) )
import Language.Haskell.TH.Syntax
$( do stuff < [ if True then 10 else 15 ]
runIO $ print stuff
return [] )
```
then I get errors about `ifThenElse` and `fromInteger` not being in scope. When I bring them into scope, the code is accepted, but the quoted syntax does not mention them, instead accurately reflecting the original source Haskell I wrote.
There are several problems in this story:
1. Template Haskell quotes are meant to work even in the presence of unbound identifiers.
2. Template Haskell is all about quoting (and splicing) surface syntax. Quoting should not care about `XRebindableSyntax`.
3. If we were to decide that quoting should respect `XRebindableSyntax` (I disagree with this design, to be clear), then the output of the quote is incorrect.
I propose: disable `XRebindableSyntax` within quotes. That should fix all these problems.
Other reasonable possibility: disable `XRebindableSyntax` within quotes, but use the TH combinators that are in scope (like `conE` and `appE`, etc.). I think this would be nightmarish to implement, and no one is asking for it, but it would be a consistent way forward.https://gitlab.haskell.org/ghc/ghc//issues/17971ApplicativeDo requires Monad constraint in recursive definition20200408T23:34:18ZManuel BärenzApplicativeDo requires Monad constraint in recursive definition## Summary
With some kinds of recursion, and `ApplicativeDo` enabled, a Monad constraint is required, even though `Applicative` would have been sufficient.
## Steps to reproduce
Typecheck this:
```haskell
foreverA :: Applicative f => f a > f b
foreverA fa = do
_a < fa
foreverA fa
```
The error message is:
```
Main.hs:10:3: error:
• Could not deduce (Monad f) arising from a do statement
from the context: Applicative f
bound by the type signature for:
foreverA :: forall (f :: * > *) a. Applicative f => f a > f ()
at Main.hs:8:140
Possible fix:
add (Monad f) to the context of
the type signature for:
foreverA :: forall (f :: * > *) a. Applicative f => f a > f ()
• In a stmt of a 'do' block: _a < fa
In the expression:
do _a < fa
foreverA fa
In an equation for ‘foreverA’:
foreverA fa
= do _a < fa
foreverA fa

10  _a < fa
 ^^^^^^^^
```
This can be worked around by adding `pure ()` as a last line, as pointed out by `maerwald` on IRC.
For a more involved example that doesn't have this kind of fix, consider:
```haskell
{# LANGUAGE ApplicativeDo #}
module StreamT where
 base
import Control.Arrow
data StreamT m a = StreamT { unStreamT :: m (a, StreamT m a) }
instance Functor m => Functor (StreamT m) where
fmap f = StreamT . fmap (f *** fmap f) . unStreamT
instance Applicative m => Applicative (StreamT m) where
pure a = StreamT $ pure (a, pure a)
fs <*> as = StreamT $ do
(f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')
```
Error message:
```
Main.hs:22:5: error:
• Could not deduce (Monad m) arising from a do statement
from the context: Applicative m
bound by the instance declaration at Main.hs:19:1049
Possible fix:
add (Monad m) to the context of
the type signature for:
(<*>) :: forall a b.
StreamT m (a > b) > StreamT m a > StreamT m b
or the instance declaration
• In a stmt of a 'do' block: (f, fs') < unStreamT fs
In the second argument of ‘($)’, namely
‘do (f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')’
In the expression:
StreamT
$ do (f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')

22  (f, fs') < unStreamT fs
 ^^^^^^^^^^^^^^^^^^^^^^^^
```
## Expected behavior
`ApplicativeDo` can correctly desugar this recursive definition.
## Environment
* GHC version used: 8.8
Optional:
* Operating System: NixOS (Linux)## Summary
With some kinds of recursion, and `ApplicativeDo` enabled, a Monad constraint is required, even though `Applicative` would have been sufficient.
## Steps to reproduce
Typecheck this:
```haskell
foreverA :: Applicative f => f a > f b
foreverA fa = do
_a < fa
foreverA fa
```
The error message is:
```
Main.hs:10:3: error:
• Could not deduce (Monad f) arising from a do statement
from the context: Applicative f
bound by the type signature for:
foreverA :: forall (f :: * > *) a. Applicative f => f a > f ()
at Main.hs:8:140
Possible fix:
add (Monad f) to the context of
the type signature for:
foreverA :: forall (f :: * > *) a. Applicative f => f a > f ()
• In a stmt of a 'do' block: _a < fa
In the expression:
do _a < fa
foreverA fa
In an equation for ‘foreverA’:
foreverA fa
= do _a < fa
foreverA fa

10  _a < fa
 ^^^^^^^^
```
This can be worked around by adding `pure ()` as a last line, as pointed out by `maerwald` on IRC.
For a more involved example that doesn't have this kind of fix, consider:
```haskell
{# LANGUAGE ApplicativeDo #}
module StreamT where
 base
import Control.Arrow
data StreamT m a = StreamT { unStreamT :: m (a, StreamT m a) }
instance Functor m => Functor (StreamT m) where
fmap f = StreamT . fmap (f *** fmap f) . unStreamT
instance Applicative m => Applicative (StreamT m) where
pure a = StreamT $ pure (a, pure a)
fs <*> as = StreamT $ do
(f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')
```
Error message:
```
Main.hs:22:5: error:
• Could not deduce (Monad m) arising from a do statement
from the context: Applicative m
bound by the instance declaration at Main.hs:19:1049
Possible fix:
add (Monad m) to the context of
the type signature for:
(<*>) :: forall a b.
StreamT m (a > b) > StreamT m a > StreamT m b
or the instance declaration
• In a stmt of a 'do' block: (f, fs') < unStreamT fs
In the second argument of ‘($)’, namely
‘do (f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')’
In the expression:
StreamT
$ do (f, fs') < unStreamT fs
(a, as') < unStreamT as
pure (f a, fs' <*> as')

22  (f, fs') < unStreamT fs
 ^^^^^^^^^^^^^^^^^^^^^^^^
```
## Expected behavior
`ApplicativeDo` can correctly desugar this recursive definition.
## Environment
* GHC version used: 8.8
Optional:
* Operating System: NixOS (Linux)https://gitlab.haskell.org/ghc/ghc//issues/17959Cannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type ...20200408T23:37:06ZFabio MogaveroCannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type synonym family application"Consider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #}
class A c
class B c
class (A (D c) => B (D c)) => C c where
type D c
~~~
GHC 8.6.5 compiles it like a charm, but both GHC 8.8.2 and 8.8.3 fail to compile with the following message:
~~~"compiler crash"
• Illegal type synonym family application ‘D c’ in instance:
B (D c)
• In the quantified constraint ‘A (D c) => B (D c)’
In the context: A (D c) => B (D c)
While checking the superclasses of class ‘C’
In the class declaration for ‘C’
~~~
Now, I am not sure if this is really a bug or, instead, a correction to the compiler, but I do not actually see why the snippet should fail to compile.
/label ~"needs triage"
/label ~bug
/label ~TypeFamilies
/label ~QuantifiedConstraintsConsider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #}
class A c
class B c
class (A (D c) => B (D c)) => C c where
type D c
~~~
GHC 8.6.5 compiles it like a charm, but both GHC 8.8.2 and 8.8.3 fail to compile with the following message:
~~~"compiler crash"
• Illegal type synonym family application ‘D c’ in instance:
B (D c)
• In the quantified constraint ‘A (D c) => B (D c)’
In the context: A (D c) => B (D c)
While checking the superclasses of class ‘C’
In the class declaration for ‘C’
~~~
Now, I am not sure if this is really a bug or, instead, a correction to the compiler, but I do not actually see why the snippet should fail to compile.
/label ~"needs triage"
/label ~bug
/label ~TypeFamilies
/label ~QuantifiedConstraintshttps://gitlab.haskell.org/ghc/ghc//issues/17853DuplicateRecordFields trigger false import warnings20200225T10:33:06ZparsonsmattDuplicateRecordFields trigger false import warnings## Summary
This is a bit of a tricky bug, but there's a bad interaction between `DuplicateRecordFields` and redundant import warnings.
Suppose you have a module:
```haskell
module Lib where
data X = X { name :: String }
data Y = Y { age :: Int }
```
You might want to consume that module like this:
```haskell
module Main where
import qualified Lib
import qualified Lib as X (X(..))
import qualified Lib as Y (Y(..))
main :: IO ()
main = do
let x = Lib.X { X.name = "hello" }
print x
print $ Lib.Y { Y.age = 3 }
```
This compiles just fine. But, suppose you add the `{# LANGUAGE DuplicateRecordFields #}` pragma to the top of the file. It will now give you a warning:
```
/home/matt/Projects/dupfield/app/Main.hs:6:1: warning: [Wunusedimports]
The qualified import of ‘Lib’ is redundant
except perhaps to import instances from ‘Lib’
To import instances alone, use: import Lib()

6  import qualified Lib as X (X(..))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/home/matt/Projects/dupfield/app/Main.hs:7:1: warning: [Wunusedimports]
The qualified import of ‘Lib’ is redundant
except perhaps to import instances from ‘Lib’
To import instances alone, use: import Lib()

7  import qualified Lib as Y (Y(..))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
If I delete the import, then I'll get compiler errors:
```
/home/matt/Projects/dupfield/app/Main.hs:11:21: error:
Not in scope: ‘X.name’
No module named ‘X’ is imported.

11  let x = Lib.X { X.name = "hello" }
 ^^^^^^
/home/matt/Projects/dupfield/app/Main.hs:13:21: error:
Not in scope: ‘Y.age’
No module named ‘Y’ is imported.

13  print $ Lib.Y { Y.age = 3 }
 ^^^^^
```
It appears that using the field label as a constructor does not trigger as a "use" if `DuplicateRecordFields` is present in the module. Using it as an accessor counts, as well as using it as an update. It seems to only be creation that does not count.
Now, in the real `Lib` in our codebase, we have many uses of `DuplicateRecordFields`, but that's actually not necessary to trigger the bug, and so it's trimmed out. We use `DuplicateRecordFields` enough that it's a defaultextension in our cabal file.
## Steps to reproduce
I made a reproduction [here](https://github.com/parsonsmatt/dupfield). To reproduce, `stack build fast filewatch`. I made some comments in the `app/Main.hs` module, feel free to play with commenting out various parts of the file to see behavior change.
## Expected behavior
I expect that using a field label in record construction syntax would not warn that the identifier isn't used.
## Environment
* GHC version used: 8.8.2
Optional:
* Operating System: Ubuntu 18.04
* Stackage LTS15.0## Summary
This is a bit of a tricky bug, but there's a bad interaction between `DuplicateRecordFields` and redundant import warnings.
Suppose you have a module:
```haskell
module Lib where
data X = X { name :: String }
data Y = Y { age :: Int }
```
You might want to consume that module like this:
```haskell
module Main where
import qualified Lib
import qualified Lib as X (X(..))
import qualified Lib as Y (Y(..))
main :: IO ()
main = do
let x = Lib.X { X.name = "hello" }
print x
print $ Lib.Y { Y.age = 3 }
```
This compiles just fine. But, suppose you add the `{# LANGUAGE DuplicateRecordFields #}` pragma to the top of the file. It will now give you a warning:
```
/home/matt/Projects/dupfield/app/Main.hs:6:1: warning: [Wunusedimports]
The qualified import of ‘Lib’ is redundant
except perhaps to import instances from ‘Lib’
To import instances alone, use: import Lib()

6  import qualified Lib as X (X(..))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/home/matt/Projects/dupfield/app/Main.hs:7:1: warning: [Wunusedimports]
The qualified import of ‘Lib’ is redundant
except perhaps to import instances from ‘Lib’
To import instances alone, use: import Lib()

7  import qualified Lib as Y (Y(..))
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
If I delete the import, then I'll get compiler errors:
```
/home/matt/Projects/dupfield/app/Main.hs:11:21: error:
Not in scope: ‘X.name’
No module named ‘X’ is imported.

11  let x = Lib.X { X.name = "hello" }
 ^^^^^^
/home/matt/Projects/dupfield/app/Main.hs:13:21: error:
Not in scope: ‘Y.age’
No module named ‘Y’ is imported.

13  print $ Lib.Y { Y.age = 3 }
 ^^^^^
```
It appears that using the field label as a constructor does not trigger as a "use" if `DuplicateRecordFields` is present in the module. Using it as an accessor counts, as well as using it as an update. It seems to only be creation that does not count.
Now, in the real `Lib` in our codebase, we have many uses of `DuplicateRecordFields`, but that's actually not necessary to trigger the bug, and so it's trimmed out. We use `DuplicateRecordFields` enough that it's a defaultextension in our cabal file.
## Steps to reproduce
I made a reproduction [here](https://github.com/parsonsmatt/dupfield). To reproduce, `stack build fast filewatch`. I made some comments in the `app/Main.hs` module, feel free to play with commenting out various parts of the file to see behavior change.
## Expected behavior
I expect that using a field label in record construction syntax would not warn that the identifier isn't used.
## Environment
* GHC version used: 8.8.2
Optional:
* Operating System: Ubuntu 18.04
* Stackage LTS15.0https://gitlab.haskell.org/ghc/ghc//issues/17768ApplicativeDo breaks compilation with a rank2 let20200625T10:02:38ZKirill Elaginkirelagin@gmail.comApplicativeDo breaks compilation with a rank2 let## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```
{# LANGUAGE ApplicativeDo, Rank2Types #}
module Test where
type M = forall m. Monad m => m () > m ()
runM :: M > IO ()
runM m = m $ pure ()
q :: IO ()
q = do
() < pure ()
let
m :: M
m = id
() < pure ()
runM m
 pure ()
```
Note that the example is very fragile. It will start to compile if you either:
* Remove `ApplicativeDo`
* Uncomment the last `pure`
* Remove one of the `pure`
* Reorder the `pure`s and `let`
The error is:
```
foo.hs:14:34: error:
• Ambiguous type variable ‘m0’ arising from a use of ‘m’
prevents the constraint ‘(Monad m0)’ from being solved.
<...>
• In the first argument of ‘return’, namely ‘m’
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
In an equation for ‘q’:
q = do () < pure ()
let m :: M
....
() < pure ()
runM m

14  () < pure ()
 ^^
foo.hs:19:8: error:
• Couldn't match type ‘m’ with ‘m0’
‘m’ is a rigid type variable bound by
a type expected by the context:
M
at foo.hs:19:38
Expected type: m () > m ()
Actual type: m0 () > m0 ()
• In the first argument of ‘runM’, namely ‘m’
In a stmt of a 'do' block: runM m
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
• Relevant bindings include
m :: m0 () > m0 () (bound at foo.hs:17:5)

19  runM m
```
The renamer outputs:
```
= do join (m_aXe < do () < pure ()
let m_aXe :: Test.M
m_aXe = id
return m_aXe 
() < pure ())
Test.runM m_aXe
```
which I couldn’t make sense of, but it looks like it is getting deshugared to something like:
```
q2 :: IO ()
q2 = let {m :: M; m = id} in return m >>= runM
```
which doesn’t compile indeed.
## Expected behavior
Code that compiles without `ApplicativeDo` should compile with `ApplicativeDo`.
## Environment
* GHC version used: 8.6.5, 8.8.2
Optional:
* Operating System:
* System Architecture:## Summary
A valid code that uses a let binding with an explicit Rank2 type stops compiling when `ApplicativeDo` is enabled.
## Steps to reproduce
```
{# LANGUAGE ApplicativeDo, Rank2Types #}
module Test where
type M = forall m. Monad m => m () > m ()
runM :: M > IO ()
runM m = m $ pure ()
q :: IO ()
q = do
() < pure ()
let
m :: M
m = id
() < pure ()
runM m
 pure ()
```
Note that the example is very fragile. It will start to compile if you either:
* Remove `ApplicativeDo`
* Uncomment the last `pure`
* Remove one of the `pure`
* Reorder the `pure`s and `let`
The error is:
```
foo.hs:14:34: error:
• Ambiguous type variable ‘m0’ arising from a use of ‘m’
prevents the constraint ‘(Monad m0)’ from being solved.
<...>
• In the first argument of ‘return’, namely ‘m’
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
In an equation for ‘q’:
q = do () < pure ()
let m :: M
....
() < pure ()
runM m

14  () < pure ()
 ^^
foo.hs:19:8: error:
• Couldn't match type ‘m’ with ‘m0’
‘m’ is a rigid type variable bound by
a type expected by the context:
M
at foo.hs:19:38
Expected type: m () > m ()
Actual type: m0 () > m0 ()
• In the first argument of ‘runM’, namely ‘m’
In a stmt of a 'do' block: runM m
In the expression:
do () < pure ()
let m :: M
m = id
() < pure ()
runM m
• Relevant bindings include
m :: m0 () > m0 () (bound at foo.hs:17:5)

19  runM m
```
The renamer outputs:
```
= do join (m_aXe < do () < pure ()
let m_aXe :: Test.M
m_aXe = id
return m_aXe 
() < pure ())
Test.runM m_aXe
```
which I couldn’t make sense of, but it looks like it is getting deshugared to something like:
```
q2 :: IO ()
q2 = let {m :: M; m = id} in return m >>= runM
```
which doesn’t compile indeed.
## Expected behavior
Code that compiles without `ApplicativeDo` should compile with `ApplicativeDo`.
## Environment
* GHC version used: 8.6.5, 8.8.2
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc//issues/17670Levitypolymorphism checker is too aggressive for uses of `coerce` on levity...20200619T14:05:21ZAlexis KingLevitypolymorphism checker is too aggressive for uses of `coerce` on levitypolymorphic newtypesGHC 8.10.1alpha2 rejects this program:
```haskell
{# LANGUAGE DataKinds, FlexibleContexts, MagicHash, PolyKinds, RankNTypes, StandaloneKindSignatures, TypeFamilies, UnliftedNewtypes #}
module M where
import Data.Coerce
import Data.Kind
import GHC.Exts (RuntimeRep(..), TYPE)
type UnboxedRep :: Type > RuntimeRep
type family UnboxedRep a
type Unboxed :: forall (a :: Type) > TYPE (UnboxedRep a)
type family Unboxed a
 The above definitions allow us to define, say
 type instance UnboxedRep Int = 'IntRep
 type instance Unboxed Int = Int#
 but those definitions are not necessary for this issue.
newtype N a = N (Unboxed a)
unN :: Coercible (N a) (Unboxed a) => N a > Unboxed a
unN = coerce
```
```
M.hs:22:7: error:
Cannot use function with levitypolymorphic arguments:
coerce :: N a > Unboxed a
Levitypolymorphic arguments: N a :: TYPE (UnboxedRep a)

22  unN = coerce
 ^^^^^^
```
I think the program ought to be accepted. There are no levitypolymorphic arguments here; surely the code generator has no trouble with `unN`, which simply returns a function? Indeed, both of the following definitions are accepted:
```haskell
f :: (N a > Unboxed a) > N a > Unboxed a
f = id
type C :: TYPE r1 > TYPE r2 > Constraint
class C a b where
m :: a > b
g :: C (N a) (Unboxed a) => N a > Unboxed a
g = m
```
Even more bizarre, the following instance of `C` is accepted, too:
```haskell
instance Coercible a b => C a b where
m = coerce
```
So I have no idea why `unN` is rejected, but it seems like something funny is going on with `coerce`.GHC 8.10.1alpha2 rejects this program:
```haskell
{# LANGUAGE DataKinds, FlexibleContexts, MagicHash, PolyKinds, RankNTypes, StandaloneKindSignatures, TypeFamilies, UnliftedNewtypes #}
module M where
import Data.Coerce
import Data.Kind
import GHC.Exts (RuntimeRep(..), TYPE)
type UnboxedRep :: Type > RuntimeRep
type family UnboxedRep a
type Unboxed :: forall (a :: Type) > TYPE (UnboxedRep a)
type family Unboxed a
 The above definitions allow us to define, say
 type instance UnboxedRep Int = 'IntRep
 type instance Unboxed Int = Int#
 but those definitions are not necessary for this issue.
newtype N a = N (Unboxed a)
unN :: Coercible (N a) (Unboxed a) => N a > Unboxed a
unN = coerce
```
```
M.hs:22:7: error:
Cannot use function with levitypolymorphic arguments:
coerce :: N a > Unboxed a
Levitypolymorphic arguments: N a :: TYPE (UnboxedRep a)

22  unN = coerce
 ^^^^^^
```
I think the program ought to be accepted. There are no levitypolymorphic arguments here; surely the code generator has no trouble with `unN`, which simply returns a function? Indeed, both of the following definitions are accepted:
```haskell
f :: (N a > Unboxed a) > N a > Unboxed a
f = id
type C :: TYPE r1 > TYPE r2 > Constraint
class C a b where
m :: a > b
g :: C (N a) (Unboxed a) => N a > Unboxed a
g = m
```
Even more bizarre, the following instance of `C` is accepted, too:
```haskell
instance Coercible a b => C a b where
m = coerce
```
So I have no idea why `unN` is rejected, but it seems like something funny is going on with `coerce`.https://gitlab.haskell.org/ghc/ghc//issues/17536Defaulting of RuntimeRep in type families is incorrect20200310T14:09:29ZKrzysztof GogolewskiDefaulting of RuntimeRep in type families is incorrectConsider
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies #}
import Data.Kind
import GHC.Types
data A (r :: RuntimeRep)
type family IsA r where
IsA (A _) = Char
IsA _ = Int
f :: IsA (A UnliftedRep)
f = 'a'
```
This program is rejected by ghc8.8 and master. The reason is that the type family is changed to:
```haskell
type family IsA r where
IsA (A 'LiftedRep) = Char
IsA _ = Int
```
The behavior was correct in ghc 8.6.
Credits to @facundominguez for finding the intial version of this bug.Consider
```haskell
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies #}
import Data.Kind
import GHC.Types
data A (r :: RuntimeRep)
type family IsA r where
IsA (A _) = Char
IsA _ = Int
f :: IsA (A UnliftedRep)
f = 'a'
```
This program is rejected by ghc8.8 and master. The reason is that the type family is changed to:
```haskell
type family IsA r where
IsA (A 'LiftedRep) = Char
IsA _ = Int
```
The behavior was correct in ghc 8.6.
Credits to @facundominguez for finding the intial version of this bug.https://gitlab.haskell.org/ghc/ghc//issues/17372Strange type equality solving failures with ImpredicativeTypes20200717T21:33:49ZJakob BrünkerStrange type equality solving failures with ImpredicativeTypes## Steps to reproduce
(I realize ImpredicativeTypes aren't really a feature at the moment, but reporting anyway since Simon wrote last week that tickets about it are still useful.)
```haskell
:set XImpredicativeTypes XConstraintKinds XGADTs XAllowAmbiguousTypes
 This typechecks
() :: ((Show a => Num a => Int) ~ ((Show a, Num a) => Int)) => ()
 > replace `Num a` with `(Eq a, Ord a)`
 This doesn't typecheck
 Couldn't match type ‘Ord a0 => Int’ with ‘Int’
() :: ((Show a => (Eq a, Ord a) => Int) ~ ((Show a, (Eq a, Ord a)) => Int)) => ()
type A a = (Eq a, Ord a)
 This typechecks
() :: (Eq a, Ord a) ~ A a => ()
 This doesn't typecheck
 Couldn't match type ‘()’ with ‘Ord a0 > ()’
() :: (A a => ()) ~ ((Eq a, Ord a) => ()) => ()
 > replace `Num a` with `A a` instead
 This typechecks
() :: ((Show a => A a => Int) ~ ((Show a, A a) => Int)) => ()
 Let's make a type synonym out of the entire constraint
type C c a = ((Show a => c => Int) ~ ((Show a, c) => Int))
 Now all of these typecheck:
() :: C (Num a) a => ()
() :: C (Eq a, Ord a) a => ()
() :: C (A a) a => ()
 This doesn't typecheck
() :: ((() => () => Int) ~ (((), ()) => Int)) => ()
 Let's turn this constraint into a different type synonym
type B a b = ((a => b => Int) ~ ((a, b) => Int))
 These both typecheck now:
() :: B (Show a) (Num a) => ()
() :: B () () => ()
```
This seems awfully inconsistent.
## Expected behavior
All of these examples should typecheck.
## Environment
* GHC version used: HEAD (8.9.0.20191012)## Steps to reproduce
(I realize ImpredicativeTypes aren't really a feature at the moment, but reporting anyway since Simon wrote last week that tickets about it are still useful.)
```haskell
:set XImpredicativeTypes XConstraintKinds XGADTs XAllowAmbiguousTypes
 This typechecks
() :: ((Show a => Num a => Int) ~ ((Show a, Num a) => Int)) => ()
 > replace `Num a` with `(Eq a, Ord a)`
 This doesn't typecheck
 Couldn't match type ‘Ord a0 => Int’ with ‘Int’
() :: ((Show a => (Eq a, Ord a) => Int) ~ ((Show a, (Eq a, Ord a)) => Int)) => ()
type A a = (Eq a, Ord a)
 This typechecks
() :: (Eq a, Ord a) ~ A a => ()
 This doesn't typecheck
 Couldn't match type ‘()’ with ‘Ord a0 > ()’
() :: (A a => ()) ~ ((Eq a, Ord a) => ()) => ()
 > replace `Num a` with `A a` instead
 This typechecks
() :: ((Show a => A a => Int) ~ ((Show a, A a) => Int)) => ()
 Let's make a type synonym out of the entire constraint
type C c a = ((Show a => c => Int) ~ ((Show a, c) => Int))
 Now all of these typecheck:
() :: C (Num a) a => ()
() :: C (Eq a, Ord a) a => ()
() :: C (A a) a => ()
 This doesn't typecheck
() :: ((() => () => Int) ~ (((), ()) => Int)) => ()
 Let's turn this constraint into a different type synonym
type B a b = ((a => b => Int) ~ ((a, b) => Int))
 These both typecheck now:
() :: B (Show a) (Num a) => ()
() :: B () () => ()
```
This seems awfully inconsistent.
## Expected behavior
All of these examples should typecheck.
## Environment
* GHC version used: HEAD (8.9.0.20191012)https://gitlab.haskell.org/ghc/ghc//issues/17208Trivial exhaustiveness checking for view patterns and guards20191009T08:40:38ZSebastian GrafTrivial exhaustiveness checking for view patterns and guardsAs discussed in #15753, ee should have better exhaustiveness checking for view patterns and guards. For example, I would expect the following program not to generate any warnings:
```haskell
{# OPTIONS_GHC Wincompletepatterns fforcerecomp #}
{# LANGUAGE ViewPatterns #}
module Lib where
safeLast :: [a] > Maybe a
safeLast xs
 [] < reverse xs = Nothing
 (x:_) < reverse xs = Just x
safeLast2 :: [a] > Maybe a
safeLast2 (reverse > []) = Nothing
safeLast2 (reverse > (x:_)) = Just x
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```As discussed in #15753, ee should have better exhaustiveness checking for view patterns and guards. For example, I would expect the following program not to generate any warnings:
```haskell
{# OPTIONS_GHC Wincompletepatterns fforcerecomp #}
{# LANGUAGE ViewPatterns #}
module Lib where
safeLast :: [a] > Maybe a
safeLast xs
 [] < reverse xs = Nothing
 (x:_) < reverse xs = Just x
safeLast2 :: [a] > Maybe a
safeLast2 (reverse > []) = Nothing
safeLast2 (reverse > (x:_)) = Just x
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc//issues/16730Instance decidability + Quantified Constraints20190618T06:34:27ZWill YagerInstance decidability + Quantified Constraints# Motivation
Consider the following program:
```Haskell
{# LANGUAGE RankNTypes, KindSignatures, QuantifiedConstraints #}
module Main where
class C a
data D (f :: * > *)
instance (forall b . C (f b)) => C (D f)
main = return ()
```
Compilation fails with
```
[1 of 1] Compiling Main ( test.hs, test.o )
test.hs:9:10: error:
• The constraint ‘C (f b)’
is no smaller than the instance head ‘C (D f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C (D f)’

9  instance (forall b . C (f b)) => C (D f)
```
# Proposal
Could we slightly modify the constraintsize rule to not count type variables that are bound within the constraint towards the size of the constraint? I.e. only free type variables "escaping" the constraint would count towards its size.
As a disclaimer, I am not entirely sure this is would be correct, but intuitively it seems fine. I would appreciate input from anyone with a rigorous understanding of these mechanisms.# Motivation
Consider the following program:
```Haskell
{# LANGUAGE RankNTypes, KindSignatures, QuantifiedConstraints #}
module Main where
class C a
data D (f :: * > *)
instance (forall b . C (f b)) => C (D f)
main = return ()
```
Compilation fails with
```
[1 of 1] Compiling Main ( test.hs, test.o )
test.hs:9:10: error:
• The constraint ‘C (f b)’
is no smaller than the instance head ‘C (D f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘C (D f)’

9  instance (forall b . C (f b)) => C (D f)
```
# Proposal
Could we slightly modify the constraintsize rule to not count type variables that are bound within the constraint towards the size of the constraint? I.e. only free type variables "escaping" the constraint would count towards its size.
As a disclaimer, I am not entirely sure this is would be correct, but intuitively it seems fine. I would appreciate input from anyone with a rigorous understanding of these mechanisms.https://gitlab.haskell.org/ghc/ghc//issues/16693Order of declarations affects which programs are accepted (type families and ...20200123T19:39:43ZIavor S. DiatchkiOrder of declarations affects which programs are accepted (type families and existentials)Consider the following example:
```haskell
{# LANGUAGE ExistentialQuantification, TypeFamilies #}
module Bug where
type family G n
type instance G a = F
data T = forall w. T (G w)
type family F where F = ()
 type family G n
```
GHC rejects this program, when checking if `T` is ambiguous. However, if I move the declaration of `G` to the end of the file (the declaration that is commented out), then GHC accepts the program.
I would guess that, somehow, it matters in what order things are processedif `G` is evaluated fully first, it can resolve to `()` and there is no ambiguity. However, if `G` is not evaluated, then there appears to be an ambiguity as `w` occurs under a type family.Consider the following example:
```haskell
{# LANGUAGE ExistentialQuantification, TypeFamilies #}
module Bug where
type family G n
type instance G a = F
data T = forall w. T (G w)
type family F where F = ()
 type family G n
```
GHC rejects this program, when checking if `T` is ambiguous. However, if I move the declaration of `G` to the end of the file (the declaration that is commented out), then GHC accepts the program.
I would guess that, somehow, it matters in what order things are processedif `G` is evaluated fully first, it can resolve to `()` and there is no ambiguity. However, if `G` is not evaluated, then there appears to be an ambiguity as `w` occurs under a type family.Vladislav ZavialovVladislav Zavialov