GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-01-02T05:27:44Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11534Allow class associated types to reference functional dependencies2021-01-02T05:27:44ZEdward KmettAllow class associated types to reference functional dependenciesConsider:
```hs
class Foo i j | i -> j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by t...Consider:
```hs
class Foo i j | i -> j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the \| i -\> j functional dependency on the class.
This would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| 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":"Allow class associated types to reference functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["FunctionalDependencies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider:\r\n\r\n{{{#!hs\r\nclass Foo i j | i -> j where\r\n type Bar i :: *\r\n type Bar i = j\r\n}}}\r\n\r\nThis is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the | i -> j functional dependency on the class.\r\n\r\nThis would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14198Inconsistent treatment of implicitly bound kind variables as free-floating2020-12-28T09:20:27ZRyan ScottInconsistent treatment of implicitly bound kind variables as free-floating(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
import Data.Pro...(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo = MkFoo (forall a. Proxy a)
```
There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`:
```
λ> :i Foo
data Foo = forall k. MkFoo (forall (a :: k). Proxy a)
```
This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable.
But to make things stranger, it you write out the kind of `a` explicitly:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
```
Then GHC will reject it:
```
Bug.hs:7:1: error:
Kind variable ‘k’ is implicitly bound in data type
‘Foo2’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
|
7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
So GHC's treatment is inconsistent. What should GHC do? We could:
1. Have both be an error.
2. Have both be accepted, and implicitly quantify `k` as an existential type variable
3. Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is:
```hs
MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo
```
4. Something else. When you try a similar trick with type synonyms:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
import Data.Proxy
type Foo3 = forall a. Proxy a
```
Instead of generalizing the kind of `a`, its kind will default to `Any`:
```
λ> :i Foo3
type Foo3 = forall (a :: GHC.Types.Any). Proxy a
```
Would that be an appropriate trick for data types as well?https://gitlab.haskell.org/ghc/ghc/-/issues/19051Allow named wildcards in constraints2020-12-23T15:23:55Zsheafsam.derbyshire@gmail.comAllow named wildcards in constraints```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = m...```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:1-12
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a
|
14 | named = meth
| ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the type-level inside the body of `named`.
(I came across this while thinking about #19010.)https://gitlab.haskell.org/ghc/ghc/-/issues/18689Why check for -fdefer-type-errors in metaTyVarUpdateOK?2020-12-22T13:22:39ZRichard Eisenbergrae@richarde.devWhy check for -fdefer-type-errors in metaTyVarUpdateOK?Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can f...Function `checkTypeEq` changes its behavior depending on the presence of `-fdefer-type-errors` in an obscure case around heterogeneous equalities; see the code in `go_co`. This is undocumented (in the code), and neither Simon nor I can figure out why it's done.
Task: figure this out, and either document or remove this behavior.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19010Partial type signature algorithm fails to infer constraints in the presence o...2020-12-20T03:26:43Zsheafsam.derbyshire@gmail.comPartial type signature algorithm fails to infer constraints in the presence of GADTsI've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of informati...I've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a -> Float
class D a where
methD :: a -> Float
foo :: forall bool a. _ => SBool bool -> a -> Float
foo sBool a = meth a
where
meth :: _ => a -> Float
meth = case sBool of
STrue -> methC
SFalse -> methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:7-11
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool -> a -> Float
* In the expression: methC
In a case alternative: STrue -> methC
In the expression:
case sBool of
STrue -> methC
SFalse -> methD
|
23 | STrue -> methC
| ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:7-12
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool -> a -> Float
* In the expression: methD
In a case alternative: SFalse -> methD
In the expression:
case sBool of
STrue -> methC
SFalse -> methD
|
24 | SFalse -> methD
| ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).https://gitlab.haskell.org/ghc/ghc/-/issues/19060Make the canonicaliser do unification2020-12-14T15:23:24ZSimon Peyton JonesMake the canonicaliser do unificationLook at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `check...Look at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `checkTyVarEq`
* All this just gets the orientation right. Then we forget all that, and later, in `tryToSolveByUnification` we call `unifyTest` again. What a mess.
One thing that discouraged me was the miasma of `rewriteEqEvidence` and `rewriteCastedEquality` and do-swap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.https://gitlab.haskell.org/ghc/ghc/-/issues/17311Type family equality gets stuck on types that fail the occurs check2020-12-11T15:47:16ZisovectorType family equality gets stuck on types that fail the occurs check## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{-# LANGUAGE AllowAmbiguous...## Summary
A type family that should check two types for equality gets stuck, even though their equality would fail the occurs check.
## Steps to reproduce
The following program doesn't compile:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
module Occurs where
import Data.Functor.Identity
import Data.Proxy
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
foo = id
```
with error:
```
• Couldn't match type ‘Equal (Identity a) a’ with ‘'False’
Expected type: Proxy (Equal (Identity a) a) -> Proxy 'False
Actual type: Proxy 'False -> Proxy 'False
• In the expression: id
In an equation for ‘foo’: foo = id
• Relevant bindings include
foo :: Proxy (Equal (Identity a) a) -> Proxy 'False
(bound at /home/sandy/Vikrem.hs:14:1)
|
14 | foo = id
|
```
The `Equal` type family is stuck due to `a` being a variable, but the only way `Equal (Identity a) a ~ 'True` is for an infinite instantiation of `a`. As such, this thing should reduce.
## Expected behavior
I expect the above program to compile, with `Equal (Identity a) a` reducing to `'False`.
## Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/18873Quantified equality constraints are not used for rewriting2020-12-10T20:30:27ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But i...If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b -> b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc/-/issues/19013Type wildcard infers differently than no type signature2020-12-10T00:22:10ZdminuosoType wildcard infers differently than no type signature```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char ...```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghc-wildcard-bug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b -> String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nix-shell:~/git/ghc-wildcard-bug]$ cabal build
Build profile: -w ghc-8.8.4 -O1
In order, the following will be built (use -v for more details):
- ghc-wildcard-bug-0.1.0.0 (exe:ghc-wildcard-bug) (file Main.hs changed)
Preprocessing executable 'ghc-wildcard-bug' for ghc-wildcard-bug-0.1.0.0..
Building executable 'ghc-wildcard-bug' for ghc-wildcard-bug-0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghc-wildcard-bug/dist-newstyle/build/x86_64-linux/ghc-8.8.4/ghc-wildcard-bug-0.1.0.0/x/ghc-wildcard-bug/build/ghc-wildcard-bug/ghc-wildcard-bug-tmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use -fprint-potential-instances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10
|
15 | f o = "foo" & (g%o) .~ 10
| ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use -fprint-potential-instances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
|
15 | f o = "foo" & (g%o) .~ 10
|
```
Also tried enabling NoMonomorphismRestriction to no avail.https://gitlab.haskell.org/ghc/ghc/-/issues/10832Generalize injective type families2020-12-09T23:11:31ZJan Stolarekjan.stolarek@ed.ac.ukGeneralize injective type familiesWith injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a...With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a b r | a b -> r, r a -> b
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r)
```
Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:
```hs
type family AddTF a b = r | r a -> b where
AddTF Zero b = b
AddTF (Succ a) b = Succ (AddTF a b)
```
But we want to be able to say that.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Generalize injective type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:\r\n\r\n{{{#!hs\r\ndata Nat = Zero | Succ a\r\n\r\nclass Add a b r | a b -> r, r a -> b\r\ninstance Add Zero b b\r\ninstance (Add a b r) => Add (Succ a) b (Succ r)\r\n}}}\r\nHere we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:\r\n\r\n{{{#!hs\r\ntype family AddTF a b = r | r a -> b where\r\n AddTF Zero b = b\r\n AddTF (Succ a) b = Succ (AddTF a b)\r\n}}}\r\nBut we want to be able to say that.","type_of_failure":"OtherFailure","blocking":[]} -->Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/15351QuantifiedConstraints ignore FunctionalDependencies2020-12-03T08:24:56ZaaronvargoQuantifiedConstraints ignore FunctionalDependenciesThe following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
...The following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with top-level instances:
```hs
instance C [a] Int where ...
baz :: [a] -> String
baz = show . foo
```https://gitlab.haskell.org/ghc/ghc/-/issues/16887GHC panic: "StgCmmEnv: variable not found" - Something with MonoLocalBinds, t...2020-11-14T10:00:44ZBerengalGHC panic: "StgCmmEnv: variable not found" - Something with MonoLocalBinds, type inference and -fdefer-type-errors# Summary
GHC panics on some modules with GADTs enabled, top level declarations without type annotations and -fdefer-type-errors enabled.
# Steps to reproduce
The smallest module I could find to trigger the bug:
```
{-# LANGUAGE GADT...# Summary
GHC panics on some modules with GADTs enabled, top level declarations without type annotations and -fdefer-type-errors enabled.
# Steps to reproduce
The smallest module I could find to trigger the bug:
```
{-# LANGUAGE GADTs #-}
breaks = pure "anything polymorphic"
main = do
putStrLn "could be anything"
breaks
putStrLn "also could be anything"
```
Command and output:
```
▶ ghc -fdefer-type-errors Panic.hs
[1 of 1] Compiling Main ( Panic.hs, Panic.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64-unknown-linux):
StgCmmEnv: variable not found
$dMonad_a1ce
local binds for:
$trModule
whatever_rq4
$trModule1_r1p6
$trModule2_r1pj
$trModule3_r1pk
$trModule4_r1pl
sat_s1rx
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
This compiles fine without `-fdefer-type-errors`, or with type signatures for either `breaks` or `main`, or without GADTs enabled. GHCi loads the module without problem, but panics whenever it needs to use any symbol from the module, including unrelated symbols.
# Expected behavior
I expect GHC not to panic.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Arch linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/16371GHC should be more forgiving with visible dependent quantification in visible...2020-11-09T15:26:20ZRyan ScottGHC should be more forgiving with visible dependent quantification in visible type applicationsGHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
imp...GHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x -> x -> Type). Proxy a
g = f @(forall x -> x -> Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x -> x -> *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x -> x -> Type). Proxy a
|
14 | g :: forall (a :: forall x -> x -> Type). Proxy a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x -> x -> *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a -> a -> a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.9 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x -> x -> Type). Proxy a\r\ng = f @(forall x -> x -> Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x -> x -> *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x -> x -> Type). Proxy a\r\n |\r\n14 | g :: forall (a :: forall x -> x -> Type). Proxy a\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x -> x -> *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a -> a -> a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/18850Instance/given overlap trips up the ambiguity check2020-10-29T19:00:42ZRichard Eisenbergrae@richarde.devInstance/given overlap trips up the ambiguity checkThursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) ...Thursday is a good day to abuse GHC. So I said this:
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:6-32
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #-}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted -- no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an over-eager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is error-free. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
| not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
| xopt LangExt.MonoLocalBinds dflags
= return ()
| ...
```
where the `...` includes generating a warning. Of course, I *do* have `-XMonoLocalBinds`, as implied by `-XTypeFamilies`. What happens when I disable this (with an explicit `-XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
-- Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()
|
11 | f :: (C bool, IsBool bool) => ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `-XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.https://gitlab.haskell.org/ghc/ghc/-/issues/10776DataKinds promotion of String -> Symbol and Natural -> Nat2020-10-28T13:07:08ZhtebalakaDataKinds promotion of String -> Symbol and Natural -> NatExactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :...Exactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :: Y ('X "hello" 4)
```
I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.https://gitlab.haskell.org/ghc/ghc/-/issues/7668Location in -fdefer-type-errors2020-09-25T17:19:16ZKrzysztof GogolewskiLocation in -fdefer-type-errorsConsider
```
x :: Char
x = 'x' + 1
y :: Char
y = 'y' + 1
```
Run `ghci -fdefer-type-errors`:
```
*Main> x
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equa...Consider
```
x :: Char
x = 'x' + 1
y :: Char
y = 'y' + 1
```
Run `ghci -fdefer-type-errors`:
```
*Main> x
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
*Main> y
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
```
The first exception is wrong. It seems that the missing `Num Char` instance is filled with the same error message in all places where the constraint should be supplied.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Location in -fdefer-type-errors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\nx :: Char\r\nx = 'x' + 1\r\n\r\ny :: Char\r\ny = 'y' + 1\r\n}}}\r\n\r\nRun `ghci -fdefer-type-errors`:\r\n\r\n{{{\r\n*Main> x\r\n*** Exception: G.hs:5:9:\r\n No instance for (Num Char) arising from a use of `+'\r\n In the expression: 'y' + 1\r\n In an equation for `y': y = 'y' + 1\r\n(deferred type error)\r\n*Main> y\r\n*** Exception: G.hs:5:9:\r\n No instance for (Num Char) arising from a use of `+'\r\n In the expression: 'y' + 1\r\n In an equation for `y': y = 'y' + 1\r\n(deferred type error)\r\n}}}\r\n\r\nThe first exception is wrong. It seems that the missing `Num Char` instance is filled with the same error message in all places where the constraint should be supplied.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/8808ImpredicativeTypes type checking fails depending on syntax of arguments2020-09-24T19:30:28ZguestImpredicativeTypes type checking fails depending on syntax of argumentsg1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.
```
{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
module Test where
f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int]...g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.
```
{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
module Test where
f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f1 (Just g) = Just (g [3], g "hello")
f1 Nothing = Nothing
f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])
f2 [g] = Just (g [3], g "hello")
f2 [] = Nothing
g1 = (f1 . Just) reverse
g1' = f1 (Just reverse)
g2 = f2 [reverse]
g2' = f2 ((:[]) reverse)
g2'' = f2 (reverse : [])
```
Compiling it with HEAD gives these errors:
```
[1 of 1] Compiling Test ( test.hs, test.o )
test.hs:12:16:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a2] -> [a2]’
In the first argument of ‛Just’, namely ‛reverse’
In the first argument of ‛f1’, namely ‛(Just reverse)’
test.hs:15:17:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a0] -> [a0]’
In the first argument of ‛: []’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛((: []) reverse)’
test.hs:16:12:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a1] -> [a1]’
In the first argument of ‛(:)’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛(reverse : [])’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.1-rc1 |
| 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":"ImpredicativeTypes type checking fails depending on syntax of arguments","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.\r\n{{{\r\n{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}\r\nmodule Test where\r\nf1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])\r\nf1 (Just g) = Just (g [3], g \"hello\")\r\nf1 Nothing = Nothing\r\n\r\nf2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])\r\nf2 [g] = Just (g [3], g \"hello\")\r\nf2 [] = Nothing\r\n\r\ng1 = (f1 . Just) reverse\r\ng1' = f1 (Just reverse)\r\n\r\ng2 = f2 [reverse]\r\ng2' = f2 ((:[]) reverse)\r\ng2'' = f2 (reverse : [])\r\n}}}\r\nCompiling it with HEAD gives these errors:\r\n{{{\r\n[1 of 1] Compiling Test ( test.hs, test.o )\r\n\r\ntest.hs:12:16:\r\n Couldn't match expected type ‛forall a. [a] -> [a]’\r\n with actual type ‛[a2] -> [a2]’\r\n In the first argument of ‛Just’, namely ‛reverse’\r\n In the first argument of ‛f1’, namely ‛(Just reverse)’\r\n\r\ntest.hs:15:17:\r\n Couldn't match expected type ‛forall a. [a] -> [a]’\r\n with actual type ‛[a0] -> [a0]’\r\n In the first argument of ‛: []’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛((: []) reverse)’\r\n\r\ntest.hs:16:12:\r\n Couldn't match expected type ‛forall a. [a] -> [a]’\r\n with actual type ‛[a1] -> [a1]’\r\n In the first argument of ‛(:)’, namely ‛reverse’\r\n In the first argument of ‛f2’, namely ‛(reverse : [])’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7828RebindableSyntax and Arrow2020-09-22T08:14:45ZAlessandroVermeulenRebindableSyntax and ArrowWhen trying to add constraints to the types of the arrow primitives I get a type error. I think that doing such a thing should be possible and I've attached the code I used to test this. The errors I get when using the arrow notation for...When trying to add constraints to the types of the arrow primitives I get a type error. I think that doing such a thing should be possible and I've attached the code I used to test this. The errors I get when using the arrow notation for the function test are as follows:
```
test :: Typeable a => R a a
test = proc n -> returnA -< n
```
```
bug-arrow.hs:15:8:
Could not deduce (Typeable c) arising from a use of `arr'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable c) to the context of
a type expected by the context: (b -> c) -> R b c
or the type signature for test :: Typeable a => R a a
In the expression: arr
When checking that `arr' (needed by a syntactic construct)
has the required type: forall b1 c1. (b1 -> c1) -> R b1 c1
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
bug-arrow.hs:15:8:
Could not deduce (Typeable c) arising from a use of `>>>'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable c) to the context of
a type expected by the context: R a1 b -> R b c -> R a1 c
or the type signature for test :: Typeable a => R a a
In the expression: (>>>)
When checking that `(>>>)' (needed by a syntactic construct)
has the required type: forall a2 b1 c1.
R a2 b1 -> R b1 c1 -> R a2 c1
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
bug-arrow.hs:15:8:
Could not deduce (Typeable d) arising from a use of `first'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable d) to the context of
a type expected by the context: R b c -> R (b, d) (c, d)
or the type signature for test :: Typeable a => R a a
In the expression: first
When checking that `first' (needed by a syntactic construct)
has the required type: forall b1 c1 d1.
R b1 c1 -> R (b1, d1) (c1, d1)
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
```
When I replace the definition with the translated core code (minus type applications and scoped type variables) the code compiles:
```
test :: Typeable a => R a a
test =
(>>>)
(arr (\ (n_apd) -> n_apd))
((>>>)
(arr (\ (ds_dst) -> ds_dst))
(returnA)
)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"RebindableSyntax and Arrow","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to add constraints to the types of the arrow primitives I get a type error. I think that doing such a thing should be possible and I've attached the code I used to test this. The errors I get when using the arrow notation for the function test are as follows:\r\n\r\n{{{\r\ntest :: Typeable a => R a a\r\ntest = proc n -> returnA -< n\r\n}}}\r\n\r\n{{{\r\nbug-arrow.hs:15:8:\r\n Could not deduce (Typeable c) arising from a use of `arr'\r\n from the context (Typeable a)\r\n bound by the type signature for test :: Typeable a => R a a\r\n at bug-arrow.hs:14:9-27\r\n Possible fix:\r\n add (Typeable c) to the context of\r\n a type expected by the context: (b -> c) -> R b c\r\n or the type signature for test :: Typeable a => R a a\r\n In the expression: arr\r\n When checking that `arr' (needed by a syntactic construct)\r\n has the required type: forall b1 c1. (b1 -> c1) -> R b1 c1\r\n arising from a proc expression at bug-arrow.hs:15:8-29\r\n In the expression: proc n -> returnA -< n\r\n\r\nbug-arrow.hs:15:8:\r\n Could not deduce (Typeable c) arising from a use of `>>>'\r\n from the context (Typeable a)\r\n bound by the type signature for test :: Typeable a => R a a\r\n at bug-arrow.hs:14:9-27\r\n Possible fix:\r\n add (Typeable c) to the context of\r\n a type expected by the context: R a1 b -> R b c -> R a1 c\r\n or the type signature for test :: Typeable a => R a a\r\n In the expression: (>>>)\r\n When checking that `(>>>)' (needed by a syntactic construct)\r\n has the required type: forall a2 b1 c1.\r\n R a2 b1 -> R b1 c1 -> R a2 c1\r\n arising from a proc expression at bug-arrow.hs:15:8-29\r\n In the expression: proc n -> returnA -< n\r\n\r\nbug-arrow.hs:15:8:\r\n Could not deduce (Typeable d) arising from a use of `first'\r\n from the context (Typeable a)\r\n bound by the type signature for test :: Typeable a => R a a\r\n at bug-arrow.hs:14:9-27\r\n Possible fix:\r\n add (Typeable d) to the context of\r\n a type expected by the context: R b c -> R (b, d) (c, d)\r\n or the type signature for test :: Typeable a => R a a\r\n In the expression: first\r\n When checking that `first' (needed by a syntactic construct)\r\n has the required type: forall b1 c1 d1.\r\n R b1 c1 -> R (b1, d1) (c1, d1)\r\n arising from a proc expression at bug-arrow.hs:15:8-29\r\n In the expression: proc n -> returnA -< n\r\n}}}\r\n\r\nWhen I replace the definition with the translated core code (minus type applications and scoped type variables) the code compiles:\r\n\r\n{{{\r\ntest :: Typeable a => R a a\r\ntest =\r\n (>>>)\r\n (arr (\\ (n_apd) -> n_apd))\r\n ((>>>)\r\n (arr (\\ (ds_dst) -> ds_dst))\r\n (returnA)\r\n )\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18456"equirecursive" type family leads to stack overflow in ghci2020-07-17T13:59:54ZXia Li-yao"equirecursive" type family leads to stack overflow in ghci## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to r...## Summary
Trying to typecheck a term using a (silly) type family such that `T ~ Maybe T` leads to a stack overflow (instead of a proper type error from reaching the max reduction depth, if this is to be an error at all).
## Steps to reproduce
```
> :set -XTypeFamilies -XUndecidableInstances
> type family T where T = Maybe T
> :t Nothing @T
Nothing @T*** Exception: stack overflow
```
(where the exception takes a few seconds to appear)
Compare that output to this variant that immediately produces a proper type error:
```
> :t Nothing @T :: T
<interactive>:5:1 error:
...
```
## Expected behavior
Either a success (`Nothing @T` has type `Maybe T` without requiring any type conversion), or a type error instead of an internal exception.
## Environment
* GHC version used: 8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/17719Note [Do not add duplicate quantified instances] is simplistic, causing rejec...2020-07-14T19:14:38ZRichard Eisenbergrae@richarde.devNote [Do not add duplicate quantified instances] is simplistic, causing rejection of programsCopied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #-}
module Bug where
class C1 a...Copied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #-}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a -> Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z -- from the C2 a constraint
[G] g2 :: forall y z. C1 z -- from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicate-elimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
-}
```
which is duly implemented. However, here, we don't have duplicates -- we have near-duplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).