GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200805T16:54:27Zhttps://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/17190Backpack signatures fail to compile when referencing class associated types w...20191125T22:37:37ZEdward KmettBackpack signatures fail to compile when referencing class associated types with defaults## Summary
Backpack signatures fail to compile when they reference class associated types with default definitions.
## Steps to reproduce
Build a library that contains a class associated type along with a default definition and require an instance of that class in a backpack signature.
Example:
`backpacktest.cabal`:
```
cabalversion: 2.4
name: backpacktest
version: 0
library common
builddepends: base
defaultlanguage: Haskell2010
exposedmodules: Class
hssourcedirs: common
library consumer
builddepends: base, common
defaultlanguage: Haskell2010
signatures: Instance
hssourcedirs: consumer
```
`common/Class.hs`:
```haskell
{# language TypeFamilies #}
module Class where
class C x where
type T x
type T x = ()
```
`consumer/Instance.hsig`:
```haskell
signature Instance where
import Class
data I
instance C I
```
Error given:
```
<no location info>: error:
The identifier R:TI does not exist in the local signature.
(Try adding it to the export list of the hsig file.)
```
Note: Removing the default `type T x = ()` results in this code compiling.
## Expected behavior
I'd expect this to work.
## Environment
* GHC version used: 8.8
Optional:
* Operating System: All
* System Architecture: All## Summary
Backpack signatures fail to compile when they reference class associated types with default definitions.
## Steps to reproduce
Build a library that contains a class associated type along with a default definition and require an instance of that class in a backpack signature.
Example:
`backpacktest.cabal`:
```
cabalversion: 2.4
name: backpacktest
version: 0
library common
builddepends: base
defaultlanguage: Haskell2010
exposedmodules: Class
hssourcedirs: common
library consumer
builddepends: base, common
defaultlanguage: Haskell2010
signatures: Instance
hssourcedirs: consumer
```
`common/Class.hs`:
```haskell
{# language TypeFamilies #}
module Class where
class C x where
type T x
type T x = ()
```
`consumer/Instance.hsig`:
```haskell
signature Instance where
import Class
data I
instance C I
```
Error given:
```
<no location info>: error:
The identifier R:TI does not exist in the local signature.
(Try adding it to the export list of the hsig file.)
```
Note: Removing the default `type T x = ()` results in this code compiling.
## Expected behavior
I'd expect this to work.
## Environment
* GHC version used: 8.8
Optional:
* Operating System: All
* System Architecture: AllJohn EricsonJohn Ericsonhttps://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