GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-02-25T01:04:53Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17405TypeFamilyDependencies aggressively requires UndecidableInstances on GHC HEAD2020-02-25T01:04:53ZRyan ScottTypeFamilyDependencies aggressively requires UndecidableInstances on GHC HEADI originally noticed this as the `singletons` library fails to compile with GHC HEAD. I will try to minimize the sources of breakage as much as possible. First, consider this module:
```hs
{-# LANGUAGE TypeFamilyDependencies #-}
module ...I originally noticed this as the `singletons` library fails to compile with GHC HEAD. I will try to minimize the sources of breakage as much as possible. First, consider this module:
```hs
{-# LANGUAGE TypeFamilyDependencies #-}
module A where
data D a
type family F a = r | r -> a
type instance F (D a) = D (F a)
```
This compiles without issue on GHC 8.8.1 and earlier, but on HEAD it fails with:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:6:15: error:
Type family equation violates injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
Using UndecidableInstances might help
In the type family equation:
F (D a) = D (F a) -- Defined at A.hs:6:15
|
6 | type instance F (D a) = D (F a)
| ^
```
That's a strange error, as I would have expected `F`'s injectivity to be sufficient to determine what `a` would be in that instance. That alone is probably enough to be considered a regression. Thankfully, that buglet is easy enough to work around: just add `{-# LANGUAGE UndecidableInstances #-}` to `A.hs` and it compiles again on HEAD.
However, things get even worse from here. Let's add two more modules into the mix:
```hs
{-# LANGUAGE TypeFamilyDependencies #-}
module B where
type family F2 a
type instance F2 Int = Bool
```
```hs
module C where
import A
import B
```
If I try to compile `C`, I get a _really_ baffling error:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive C.hs
GHCi, version 8.9.0.20191023: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 3] Compiling A ( A.hs, interpreted )
[2 of 3] Compiling B ( B.hs, interpreted )
[3 of 3] Compiling C ( C.hs, interpreted )
A.hs:7:15: error:
Type family equation violates injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
Using UndecidableInstances might help
In the type family equation:
F (D a) = D (F a) -- Defined at A.hs:7:15
|
7 | type instance F (D a) = D (F a)
| ^
Failed, two modules loaded.
```
You're reading that right: when compiling `C.hs`, I get an error message that points to a line of code in `A.hs`. Wat. This definitely seems like a bug.
What's curious is that defining a `type instance` in `B.hs` appears to be essential to triggering this bug. If I comment out the `type instance F2 Int = Bool` part, then compiling `C.hs` works without a hitch.
Like before, you can work around the issue by adding `{-# LANGUAGE UndecidableInstances #-}` to `C.hs`. This is really cumbersome, however, because it effectively means one has to enable this language extension in every module that imports `A` and another type family. In the particular case of the `singletons` library, this translates to enabling `UndecidableInstances` in almost every single module.
I'm almost positive this regression was introduced in 1cd3fa299c85f1b324c22288669c75246e3bc575, so cc'ing @rae.8.10.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17077"Quantification by level numbers would fail" for an ill-kinded signature2019-09-24T16:49:34ZVladislav Zavialov"Quantification by level numbers would fail" for an ill-kinded signature## Summary
With assertions enabled, this program causes a warning about level numbers:
```haskell
{-# LANGUAGE RankNTypes, PolyKinds #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module T where
import Data.Proxy
t :: Proxy (z :: for...## Summary
With assertions enabled, this program causes a warning about level numbers:
```haskell
{-# LANGUAGE RankNTypes, PolyKinds #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module T where
import Data.Proxy
t :: Proxy (z :: forall k. a)
t = t
```
The warning and the kind error are as follows:
```
WARNING: file compiler/typecheck/TcMType.hs, line 1472
Quantification by level numbers would fail
Outer level = 0
dep_tkvs = {k_a1f6[tau:0], k_a1f7[tau:0], a_a1eI[sk:1],
k_a1f4[tau:1]}
co_vars = co_a1f3 :: k_a1eK[tau:1]
~# (forall (k :: k_a1eX[tau:1]). a_a1eI[sk:1])
co_tvs = {a_a1eI[sk:1], k_a1eK[tau:1], k_a1eX[tau:1], co_a1f3}
dep_kvs = [k_a1f4[tau:1]]
dep_kvs2 = [a_a1eI[sk:1], k_a1f4[tau:1]]
nondep_tvs = []
nondep_tvs2 = []
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1237:29 in ghc:Outputable
warnPprTrace, called at compiler/typecheck/TcMType.hs:1472:11 in ghc:TcMType
Bug.hs:7:13: error:
• Expected kind ‘forall (k :: k1). a’, but ‘z’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely ‘(z :: forall k. a)’
In the type signature: t :: Proxy (z :: forall k. a)
|
7 | t :: Proxy (z :: forall k. a)
|
```
## Steps to reproduce
1. Compile GHC with assertions enabled (`hadrian/build.sh -j --flavour=Devel2`).
2. Load the aforementioned program in GHCi (`_build/stage1/bin/ghc --interactive`)
## Expected behavior
No warning.
## Environment
* GHC version used: HEAD8.10.1Simon Peyton JonesRichard Eisenbergrae@richarde.devSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/16728GHC HEAD-only panic with PartialTypeSignatures2019-07-07T18:00:04ZRyan ScottGHC HEAD-only panic with PartialTypeSignaturesThe following program typechecks on GHC 8.8.1:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = ...The following program typechecks on GHC 8.8.1:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [-Wpartial-type-signatures]ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.8.10.1Ryan ScottRichard Eisenbergrae@richarde.devRyan Scott