GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:40Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11376Inconsistent specified type variables among functions and datatypes/classes w...2019-07-07T18:30:40ZRyan ScottInconsistent specified type variables among functions and datatypes/classes when using -XTypeApplicationsOriginally reported [here](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010915.html). When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using ...Originally reported [here](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010915.html). When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using functions, datatypes, or typeclasses.
Here's an example contrasting functions and datatypes:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help
λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType
λ> data Prox a = Prox
λ> prox :: Prox a; prox = Prox
λ> :t prox
prox :: forall k (a :: k). Prox k a
λ> :t prox @Int
prox @Int :: Prox * Int
λ> :t Prox
Prox :: forall k (a :: k). Prox k a
λ> :t Prox @Int
Prox @Int :: Prox Int a
```
This is the core of the problem: with a function, `Int` seems to be applied to type variable `a`, whereas with data types, `Int` appears to be applied to the kind variable `k`. This confuses me, since `k` wasn't specified anywhere in the definition of `Prox`.
Andres Löh also [observed](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010916.html) a similar discrepancy between functions and typeclasses:
```
λ> :set -XScopedTypeVariables
λ> class C a where c :: ()
λ> d :: forall a. C a => (); d = c @_ @a
λ> :t d
d :: forall k (a :: k). C k a => ()
λ> :t d @Int
d @Int :: C * Int => ()
λ> :t c
c :: forall k (a :: k). C k a => ()
λ> :t c @Int
c @Int :: C Int a => ()
λ> :t c @_ @Int
c @_ @Int :: C * Int => ()
```
EDIT: See also documentation infelicity in [ticket:11376\#comment:113518](https://gitlab.haskell.org//ghc/ghc/issues/11376#note_113518).
EDIT: Most of this is fix, as of March 25. But the data family stuff in [ticket:11376\#comment:114637](https://gitlab.haskell.org//ghc/ghc/issues/11376#note_114637) is still outstanding, and we need a test case.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11385Unify named wildcards in different type applications2019-07-07T18:30:39ZIcelandjackUnify named wildcards in different type applications([motivating post](https://www.reddit.com/r/haskell/comments/4030lv/unifying_distinct_type_variables_in/))
I would like to use type application to specialize
```hs
Sub :: forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :...([motivating post](https://www.reddit.com/r/haskell/comments/4030lv/unifying_distinct_type_variables_in/))
I would like to use type application to specialize
```hs
Sub :: forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub @(Ord _a) @(Eq _a) :: forall {a}. (Ord a => Dict (Eq a)) -> Ord a :- Eq a
```
and
```hs
map :: forall a b. (a -> b) -> [a] -> [b]
map @_a @_a :: forall {a}. (a -> a) -> [a] -> [a]
```
Is there a fundamental reason why named wildcards are not allowed to unify between type applications within the same expression? [Documentation](https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#named-wildcards):
> These are called named wildcards. All occurrences of the same named wildcard within one type signature will unify to the same type.
I don't know if this is intended.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Unify named wildcards in different type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["NamedWildCards","TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"([https://www.reddit.com/r/haskell/comments/4030lv/unifying_distinct_type_variables_in/ motivating post])\r\n\r\nI would like to use type application to specialize\r\n\r\n{{{#!hs\r\nSub :: forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b\r\nSub @(Ord _a) @(Eq _a) :: forall {a}. (Ord a => Dict (Eq a)) -> Ord a :- Eq a\r\n}}}\r\n\r\nand\r\n\r\n{{{#!hs\r\nmap :: forall a b. (a -> b) -> [a] -> [b]\r\nmap @_a @_a :: forall {a}. (a -> a) -> [a] -> [a]\r\n}}}\r\n\r\nIs there a fundamental reason why named wildcards are not allowed to unify between type applications within the same expression? [https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#named-wildcards Documentation]:\r\n\r\n> These are called named wildcards. All occurrences of the same named wildcard within one type signature will unify to the same type.\r\n\r\nI don't know if this is intended.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11391TypeError is fragile2019-07-07T18:30:37ZBen GamariTypeError is fragileConsider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type fami...Consider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type family Resolve (t :: Type -> Type) :: Type -> Type where
Resolve _ = TypeError (Text "ERROR")
```
#### The okay case
Given something like,
```hs
testOK :: Resolve [] Int
testOK = []
```
we find that things work as expected,
```
• ERROR
• In the expression: [] :: Resolve [] Int
In an equation for ‘testOK’: testOK = [] :: Resolve [] Int
```
#### The bad case
However, it is very easy to fool GHC into not yielding the desired error message. For instance,
```hs
testNOTOK1 :: Resolve [] Int
testNOTOK1 = ()
```
gives us this a unification error,
```
• Couldn't match type ‘()’ with ‘(TypeError ...)’
Expected type: Resolve [] Int
Actual type: ()
```
This clearly isn't what we expected.
#### The tricky case
Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`,
```hs
testNOTOK2 :: Resolve [] Int
testNOTOK2 = 1
```
Which results in,
```
• No instance for (Num (TypeError ...))
arising from the literal ‘1’
• In the expression: 1
In an equation for ‘testNOTOK2’: testNOTOK2 = 1
```8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/11397Type mismatch in local definitions in Haskell 98 code2019-07-07T18:30:36ZLemmingType mismatch in local definitions in Haskell 98 codeHere is the affected code with all package dependencies removes:
```
$ cat PairMismatch.hs
module PairMismatch (inverseFrequencyModulationChunk) where
newtype VectorLazy a = VectorLazy a
newtype Vector a = Vector a
newtype Pointer a = ...Here is the affected code with all package dependencies removes:
```
$ cat PairMismatch.hs
module PairMismatch (inverseFrequencyModulationChunk) where
newtype VectorLazy a = VectorLazy a
newtype Vector a = Vector a
newtype Pointer a = Pointer a
empty :: VectorLazy a
empty = undefined
cons :: Vector a -> Pointer a
cons = undefined
unfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)
unfoldrResult = undefined
switchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b
switchL = undefined
inverseFrequencyModulationChunk ::
(Num t, Ord t) =>
(s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))
inverseFrequencyModulationChunk nextC (phase,cst0) chunk =
let {-
switch ::
(Maybe (t, s) -> r) ->
((t, v) -> (s, Pointer v) -> r) ->
t ->
(s, Pointer v) -> r
-}
switch l r t (cp0,xp0) =
maybe
(l Nothing)
(\(c1,cp1) ->
switchL
(l (Just (t,cp0)))
(\x1 xp1 -> r (t+c1,x1) (cp1,xp1))
xp0)
(nextC cp0)
{-
go ::
(t,v) -> (s, Pointer v) ->
Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))
-}
go (c,x) cxp =
if c<1
then switch Left go c cxp
else Right (x, ((c-1,x),cxp))
in switch ((,) empty)
(curry $ unfoldrResult (uncurry go))
phase (cst0, cons chunk)
$ ghci-8.0.0.20160109 PairMismatch.hs
GHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )
PairMismatch.hs:35:24: error:
• Couldn't match type ‘a’ with ‘(t, s)’
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at PairMismatch.hs:35:24
Expected type: forall a. Maybe a
Actual type: Maybe (t, s)
• In the first argument of ‘l’, namely ‘(Just (t, cp0))’
In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’
In the expression:
switchL
(l (Just (t, cp0))) (\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0
• Relevant bindings include
cp1 :: s (bound at PairMismatch.hs:33:20)
c1 :: t (bound at PairMismatch.hs:33:17)
cp0 :: s (bound at PairMismatch.hs:30:22)
t :: t (bound at PairMismatch.hs:30:19)
r :: (t, t1) -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:17)
switch :: ((forall a. Maybe a) -> b)
-> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b
(bound at PairMismatch.hs:30:8)
inverseFrequencyModulationChunk :: (s -> Maybe (t, s))
-> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))
(bound at PairMismatch.hs:22:1)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
Failed, modules loaded: none.
```
It works with GHC-7.10.3 and before.
I may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Type mismatch in local definitions in Haskell 98 code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is the affected code with all package dependencies removes:\r\n{{{\r\n$ cat PairMismatch.hs\r\nmodule PairMismatch (inverseFrequencyModulationChunk) where\r\n\r\nnewtype VectorLazy a = VectorLazy a\r\nnewtype Vector a = Vector a\r\nnewtype Pointer a = Pointer a\r\n\r\nempty :: VectorLazy a\r\nempty = undefined\r\n\r\ncons :: Vector a -> Pointer a\r\ncons = undefined\r\n\r\nunfoldrResult :: (a -> Either c (b, a)) -> a -> (VectorLazy b, c)\r\nunfoldrResult = undefined\r\n\r\nswitchL :: b -> (a -> Pointer a -> b) -> Pointer a -> b\r\nswitchL = undefined\r\n\r\ninverseFrequencyModulationChunk ::\r\n (Num t, Ord t) =>\r\n (s -> Maybe (t,s)) -> (t,s) -> Vector v -> (VectorLazy v, Maybe (t,s))\r\ninverseFrequencyModulationChunk nextC (phase,cst0) chunk =\r\n let {-\r\n switch ::\r\n (Maybe (t, s) -> r) ->\r\n ((t, v) -> (s, Pointer v) -> r) ->\r\n t ->\r\n (s, Pointer v) -> r\r\n -}\r\n switch l r t (cp0,xp0) =\r\n maybe\r\n (l Nothing)\r\n (\\(c1,cp1) ->\r\n switchL\r\n (l (Just (t,cp0)))\r\n (\\x1 xp1 -> r (t+c1,x1) (cp1,xp1))\r\n xp0)\r\n (nextC cp0)\r\n\r\n {-\r\n go ::\r\n (t,v) -> (s, Pointer v) ->\r\n Either (Maybe (t,s)) (v, ((t,v), (s, Pointer v)))\r\n -}\r\n go (c,x) cxp =\r\n if c<1\r\n then switch Left go c cxp\r\n else Right (x, ((c-1,x),cxp))\r\n\r\n in switch ((,) empty)\r\n (curry $ unfoldrResult (uncurry go))\r\n phase (cst0, cons chunk)\r\n\r\n$ ghci-8.0.0.20160109 PairMismatch.hs \r\nGHCi, version 8.0.0.20160109: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling PairMismatch ( PairMismatch.hs, interpreted )\r\n\r\nPairMismatch.hs:35:24: error:\r\n • Couldn't match type ‘a’ with ‘(t, s)’\r\n ‘a’ is a rigid type variable bound by\r\n a type expected by the context:\r\n forall a. Maybe a\r\n at PairMismatch.hs:35:24\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe (t, s)\r\n • In the first argument of ‘l’, namely ‘(Just (t, cp0))’\r\n In the first argument of ‘switchL’, namely ‘(l (Just (t, cp0)))’\r\n In the expression:\r\n switchL\r\n (l (Just (t, cp0))) (\\ x1 xp1 -> r (t + c1, x1) (cp1, xp1)) xp0\r\n • Relevant bindings include\r\n cp1 :: s (bound at PairMismatch.hs:33:20)\r\n c1 :: t (bound at PairMismatch.hs:33:17)\r\n cp0 :: s (bound at PairMismatch.hs:30:22)\r\n t :: t (bound at PairMismatch.hs:30:19)\r\n r :: (t, t1) -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:17)\r\n switch :: ((forall a. Maybe a) -> b)\r\n -> ((t, t1) -> (s, Pointer t1) -> b) -> t -> (s, Pointer t1) -> b\r\n (bound at PairMismatch.hs:30:8)\r\n inverseFrequencyModulationChunk :: (s -> Maybe (t, s))\r\n -> (t, s) -> Vector v -> (VectorLazy v, Maybe (t, s))\r\n (bound at PairMismatch.hs:22:1)\r\n (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)\r\nFailed, modules loaded: none.\r\n}}}\r\nIt works with GHC-7.10.3 and before.\r\nI may try to further simplify the code and choose a better ticket header, if I got an idea what went wrong.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11399Ill-kinded instance head involving -XTypeInType can invoke GHC panic2019-07-07T18:30:35ZRyan ScottIll-kinded instance head involving -XTypeInType can invoke GHC panicThis code:
```hs
{-# LANGUAGE FlexibleInstances, TypeInType #-}
module FvProvFallsIntoAHole where
import Data.Kind
newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)
instance Functor k => Functor (UhOh k) where
```
produces this GHC ...This code:
```hs
{-# LANGUAGE FlexibleInstances, TypeInType #-}
module FvProvFallsIntoAHole where
import Data.Kind
newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)
instance Functor k => Functor (UhOh k) where
```
produces this GHC panic:
```
$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs
[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160108 for x86_64-unknown-linux):
fvProv falls into a hole {aq6}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Ill-kinded instance head involving -XTypeInType can invoke GHC panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances, TypeInType #-}\r\nmodule FvProvFallsIntoAHole where\r\n\r\nimport Data.Kind\r\n\r\nnewtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *)\r\ninstance Functor k => Functor (UhOh k) where\r\n}}}\r\n\r\nproduces this GHC panic:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc FvProvFallsIntoAHole.hs\r\n[1 of 1] Compiling FvProvFallsIntoAHole ( FvProvFallsIntoAHole.hs, FvProvFallsIntoAHole.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160108 for x86_64-unknown-linux):\r\n fvProv falls into a hole {aq6}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11400* is not an indexed type family2019-07-07T18:30:35ZRyan Scott* is not an indexed type familyI can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help
λ>...I can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help
λ> :set -XTypeInType -XTypeFamilies
λ> import Data.Kind
λ> data family IdxProxy k (a :: k)
λ> data instance IdxProxy * a
<interactive>:5:1: error:
• Illegal family instance for ‘*’
(* is not an indexed type family)
• In the data instance declaration for ‘*’
λ> data instance IdxProxy Type a
λ> :kind! IdxProxy *
IdxProxy * :: * -> *
= IdxProxy *
λ> :kind! IdxProxy Type
IdxProxy Type :: Type -> *
= IdxProxy Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"* is not an indexed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"I can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci\r\nGHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XTypeInType -XTypeFamilies \r\nλ> import Data.Kind\r\nλ> data family IdxProxy k (a :: k)\r\nλ> data instance IdxProxy * a\r\n\r\n<interactive>:5:1: error:\r\n • Illegal family instance for ‘*’\r\n (* is not an indexed type family)\r\n • In the data instance declaration for ‘*’\r\nλ> data instance IdxProxy Type a\r\nλ> :kind! IdxProxy *\r\nIdxProxy * :: * -> *\r\n= IdxProxy *\r\nλ> :kind! IdxProxy Type\r\nIdxProxy Type :: Type -> *\r\n= IdxProxy Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/11407-XTypeInType uses up all memory when used in data family instance2019-07-07T18:30:33ZRyan Scott-XTypeInType uses up all memory when used in data family instanceCompiling this code with GHC 8.1 causes all my memory to be used very quickly:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data family UhOh ...Compiling this code with GHC 8.1 causes all my memory to be used very quickly:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data family UhOh (f :: k1) (a :: k2) (b :: k3)
data instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
On the other hand, this code compiles without issue:
```hs
{-# LANGUAGE TypeInType #-}
module TypeInTypeEatsAllMemory where
import Data.Kind
type Const a b = a
data UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"-XTypeInType uses up all memory when used in data family instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Compiling this code with GHC 8.1 causes all my memory to be used very quickly:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata family UhOh (f :: k1) (a :: k2) (b :: k3)\r\ndata instance UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}\r\n\r\nOn the other hand, this code compiles without issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule TypeInTypeEatsAllMemory where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\n\r\ndata UhOh (f :: * -> * -> *) (a :: forall a) (b :: Const * a) = UhOh\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11411GHC allows you to quantify variables over TYPE 'Unlifted (a.k.a, #)2019-07-07T18:30:32ZRyan ScottGHC allows you to quantify variables over TYPE 'Unlifted (a.k.a, #)This should be disallowed, so [sayeth goldfire](https://phabricator.haskell.org/D1757):
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160109: http://www.haskell.org/ghc/ :? for help
λ> :set -XKindSignatures
λ> import ...This should be disallowed, so [sayeth goldfire](https://phabricator.haskell.org/D1757):
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160109: http://www.haskell.org/ghc/ :? for help
λ> :set -XKindSignatures
λ> import GHC.Types
λ> data Wat (a :: TYPE 'Unlifted) = Wat a
λ> :i Wat
data Wat (a :: #) = Wat a -- Defined at <interactive>:3:1
λ> :set -XMagicHash
λ> :t Wat 1#
Wat 1# :: Wat GHC.Prim.Int#
λ> :t Wat 'a'#
Wat 'a'# :: Wat GHC.Prim.Char#
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC allows you to quantify variables over TYPE 'Unlifted (a.k.a, #)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This should be disallowed, so [https://phabricator.haskell.org/D1757 sayeth goldfire]:\r\n\r\n{{{\r\n$ inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160109: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XKindSignatures \r\nλ> import GHC.Types\r\nλ> data Wat (a :: TYPE 'Unlifted) = Wat a\r\nλ> :i Wat\r\ndata Wat (a :: #) = Wat a -- Defined at <interactive>:3:1\r\nλ> :set -XMagicHash \r\nλ> :t Wat 1#\r\nWat 1# :: Wat GHC.Prim.Int#\r\nλ> :t Wat 'a'#\r\nWat 'a'# :: Wat GHC.Prim.Char#\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11416GHC mistakenly believes datatype with type synonym in its type can't be eta-r...2019-07-07T18:30:31ZRyan ScottGHC mistakenly believes datatype with type synonym in its type can't be eta-reducedI uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deri...I uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor
```
This fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):
```
• Cannot eta-reduce to an instance of form
instance (...) => Functor (T f)
• In the newtype declaration for ‘T
```
But it *should* be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.
I marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:
```hs
{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}
module CantEtaReduce2 where
type ConstantT a b = a
data family T (f :: * -> *) (a :: *)
newtype instance T f (ConstantT a f) = T (f a) deriving Functor
```
I believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"I uncovered this when playing around with `-XTypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, TypeInType #-}\r\nmodule CantEtaReduce1 where\r\n\r\nimport Data.Kind\r\n\r\ntype ConstantT a b = a\r\nnewtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor\r\n}}}\r\n\r\nThis fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):\r\n\r\n{{{\r\n • Cannot eta-reduce to an instance of form\r\n instance (...) => Functor (T f)\r\n • In the newtype declaration for ‘T\r\n}}}\r\n\r\nBut it ''should'' be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.\r\n\r\nI marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}\r\nmodule CantEtaReduce2 where\r\n\r\ntype ConstantT a b = a\r\ndata family T (f :: * -> *) (a :: *)\r\nnewtype instance T f (ConstantT a f) = T (f a) deriving Functor\r\n}}}\r\n\r\nI believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11424"Occurs check" not considered when reducing closed type families2019-07-07T18:30:28ZIavor S. Diatchki"Occurs check" not considered when reducing closed type familiesHello,
consider the following example:
```hs
{-# LANGUAGE TypeFamilies #-}
type family Same a b where
Same a a = Int
Same a b = Char
example :: Same a [a] -> a
example = undefined
bad :: a
bad = example 'c'
```
This program sho...Hello,
consider the following example:
```hs
{-# LANGUAGE TypeFamilies #-}
type family Same a b where
Same a a = Int
Same a b = Char
example :: Same a [a] -> a
example = undefined
bad :: a
bad = example 'c'
```
This program should type check, using the following reasoning: `a` and `[a]` can never be equal, therefore the first equation for `Same` does not apply, and so we can fall trough to the second one, thus reducing `Same` to `Char`. Therefore, `bad` should be accept.
GHC rejects this program with the following error:
```
• Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’
• In the first argument of ‘example’, namely ‘'c'’
In the expression: example 'c'
In an equation for ‘bad’: bad = example 'c'
• Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"\"Occurs check\" not considered when reducing closed type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Hello,\r\n\r\nconsider the following example:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family Same a b where\r\n Same a a = Int\r\n Same a b = Char\r\n\r\nexample :: Same a [a] -> a\r\nexample = undefined\r\n\r\nbad :: a\r\nbad = example 'c'\r\n}}}\r\n\r\nThis program should type check, using the following reasoning: `a` and `[a]` can never be equal, therefore the first equation for `Same` does not apply, and so we can fall trough to the second one, thus reducing `Same` to `Char`. Therefore, `bad` should be accept.\r\n\r\nGHC rejects this program with the following error:\r\n{{{\r\n • Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’\r\n • In the first argument of ‘example’, namely ‘'c'’\r\n In the expression: example 'c'\r\n In an equation for ‘bad’: bad = example 'c'\r\n • Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11428ImpredicativeTypes causes GHC panic with 8.0.1-rc12019-07-07T18:30:27ZRyan ScottImpredicativeTypes causes GHC panic with 8.0.1-rc1I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [Data.Conduit.Internal.Pipe](https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs) module). This (greatly si...I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [Data.Conduit.Internal.Pipe](https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs) module). This (greatly simplified) code, which compiles without issue on GHC 7.10.3:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
module Data.Conduit.Internal.Pipe where
data Pipe o r =
HaveOutput (Pipe o r) o
mapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r
mapOutputMaybe f (HaveOutput p o) =
maybe id (\o' p' -> HaveOutput p' o') (f o) (mapOutputMaybe f p)
```
emits a GHC panic with GHC 8.0.1-rc1:
```
[1 of 1] Compiling Data.Conduit.Internal.Pipe ( Wat.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.0.20160111 for x86_64-unknown-linux):
matchExpectedFunTys
<>
a_a15Z[tau:5] -> b_a15Y[tau:5]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Note that this code does not require `-XImpredicativeTypes`, and removing the pragma makes the code compile again.
Marking as high since it's a regression, but not highest because `-XImpredicativeTypes` has long been broken (see also #11319). Still, this currently happens on code in the wild, and perhaps it would be worth turning this into a more sensible error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"ImpredicativeTypes causes GHC panic with 8.0.1-rc1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["ImpredicativeTypes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I noticed this issue when attempting to compile `conduit` with GHC 8.0.1-rc1 (specifically, the [https://github.com/snoyberg/conduit/blob/master/conduit/Data/Conduit/Internal/Pipe.hs Data.Conduit.Internal.Pipe] module). This (greatly simplified) code, which compiles without issue on GHC 7.10.3:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\nmodule Data.Conduit.Internal.Pipe where\r\n\r\ndata Pipe o r =\r\n HaveOutput (Pipe o r) o\r\n\r\nmapOutputMaybe :: (o1 -> Maybe o2) -> Pipe o1 r -> Pipe o2 r\r\nmapOutputMaybe f (HaveOutput p o) =\r\n maybe id (\\o' p' -> HaveOutput p' o') (f o) (mapOutputMaybe f p)\r\n}}}\r\n\r\nemits a GHC panic with GHC 8.0.1-rc1:\r\n\r\n{{{\r\n[1 of 1] Compiling Data.Conduit.Internal.Pipe ( Wat.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.0.20160111 for x86_64-unknown-linux):\r\n\tmatchExpectedFunTys\r\n <>\r\n a_a15Z[tau:5] -> b_a15Y[tau:5]\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nNote that this code does not require `-XImpredicativeTypes`, and removing the pragma makes the code compile again.\r\n\r\nMarking as high since it's a regression, but not highest because `-XImpredicativeTypes` has long been broken (see also #11319). Still, this currently happens on code in the wild, and perhaps it would be worth turning this into a more sensible error.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11453Kinds in type synonym/data declarations can unexpectedly unify2019-07-07T18:30:21ZRyan ScottKinds in type synonym/data declarations can unexpectedly unifyWhile trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType ...While trying out ideas to fix [this lens issue](https://github.com/ekmett/lens/issues/626), I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:
```
$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall (f :: k1 -> *). Either (f a) (f b)
-- Defined at <interactive>:2:1
```
This is pretty odd for two reasons. One, the kind `k1` was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:
```
λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
forall k2 (f :: k2 -> *). Either (f a) (f b)
-- Defined at <interactive>:4:1
```
We still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.
Note that this doesn't happen if you use explicit kind binders:
```
type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
<interactive>:6:74: error:
• Expected kind ‘k1’, but ‘a’ has kind ‘k2’
• In the first argument of ‘f’, namely ‘a’
In the first argument of ‘Either’, namely ‘f a’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
<interactive>:6:80: error:
• Expected kind ‘k1’, but ‘b’ has kind ‘k3’
• In the first argument of ‘f’, namely ‘b’
In the second argument of ‘Either’, namely ‘f b’
In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’
```
only when the kinds are specified but not visible.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds in type synonym/data declarations can unexpectedly unify","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"While trying out ideas to fix [https://github.com/ekmett/lens/issues/626 this lens issue], I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators\r\nGHCi, version 8.1.20160113: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/xnux/.ghci\r\nλ> import Data.Kind\r\nλ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall (f :: k1 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:2:1\r\n}}}\r\n\r\nThis is pretty odd for two reasons. One, the kind {{{k1}}} was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:\r\n\r\n{{{\r\nλ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\nλ> :i Wat\r\ntype Wat (a :: k1) (b :: k1) =\r\n forall k2 (f :: k2 -> *). Either (f a) (f b)\r\n -- Defined at <interactive>:4:1\r\n}}}\r\n\r\nWe still see the second issue: GHC thinks that the type variables `a` and `b` have the same kind `k1`, when they should have separate kinds `k1` and `k2`! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.\r\n\r\nNote that this doesn't happen if you use explicit kind binders:\r\n\r\n{{{\r\ntype Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)\r\n\r\n<interactive>:6:74: error:\r\n • Expected kind ‘k1’, but ‘a’ has kind ‘k2’\r\n • In the first argument of ‘f’, namely ‘a’\r\n In the first argument of ‘Either’, namely ‘f a’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n\r\n<interactive>:6:80: error:\r\n • Expected kind ‘k1’, but ‘b’ has kind ‘k3’\r\n • In the first argument of ‘f’, namely ‘b’\r\n In the second argument of ‘Either’, namely ‘f b’\r\n In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’\r\n}}}\r\n\r\nonly when the kinds are specified but not visible.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11458Terrible failure of type inference in visible type application2019-07-07T18:30:20ZSimon Peyton JonesTerrible failure of type inference in visible type applicationConsider
```
-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)
optIntArg f = (f Nothing, f (Just True))
```
This is rejected (by HEAD)
```
T11379a.hs:5:30: error:
* Couldn't match type `a' with `Bool'
`a' is a rigid type variable...Consider
```
-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)
optIntArg f = (f Nothing, f (Just True))
```
This is rejected (by HEAD)
```
T11379a.hs:5:30: error:
* Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
a type expected by the context:
forall a. Maybe a
at T11379a.hs:5:30
Expected type: forall a. Maybe a
Actual type: Maybe Bool
* In the first argument of `f', namely `(Just True)'
In the expression: f (Just True)
In the expression: (f Nothing, f (Just True))
```
but if you put the tuple components the other way round, it works fine
```
optIntArg f = (f (Just True), f Nothing)
```
Adding the commented-out signature also makes it work fine.
I'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.
I suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Terrible failure of type inference in visible type application","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)\r\noptIntArg f = (f Nothing, f (Just True))\r\n}}}\r\nThis is rejected (by HEAD)\r\n{{{\r\nT11379a.hs:5:30: error:\r\n * Couldn't match type `a' with `Bool'\r\n `a' is a rigid type variable bound by\r\n a type expected by the context:\r\n forall a. Maybe a\r\n at T11379a.hs:5:30\r\n Expected type: forall a. Maybe a\r\n Actual type: Maybe Bool\r\n * In the first argument of `f', namely `(Just True)'\r\n In the expression: f (Just True)\r\n In the expression: (f Nothing, f (Just True))\r\n}}}\r\nbut if you put the tuple components the other way round, it works fine\r\n{{{\r\noptIntArg f = (f (Just True), f Nothing)\r\n}}}\r\nAdding the commented-out signature also makes it work fine.\r\n\r\nI'm almost certain that this is caused by visible type application; perhaps `Nothing` gets delayed instantiation, and then `f`'s type becomes `forall a. Maybe a`. Utterly bogus.\r\n\r\nI suspect it'll be fixed by Richards `ReturnTv` work, but let's make sure it is. We can't release this!!\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11466Constraint synonym with Implicit Parameter2019-07-07T18:30:18ZJoachim Breitnermail@joachim-breitner.deConstraint synonym with Implicit ParameterThis:
```
{-# LANGUAGE ConstraintKinds, ImplicitParams #-}
module Foo where
type Foo = ?foo::()
```
gives
```
Foo.hs:3:1: error:
• Illegal implicit parameter ‘?foo::()’
• In the type synonym declaration for ‘Foo’
```
in GHC H...This:
```
{-# LANGUAGE ConstraintKinds, ImplicitParams #-}
module Foo where
type Foo = ?foo::()
```
gives
```
Foo.hs:3:1: error:
• Illegal implicit parameter ‘?foo::()’
• In the type synonym declaration for ‘Foo’
```
in GHC HEAD. It used to work in GHC-7.10. Did not check GHC-8.0.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Constraint synonym with Implicit Parameter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This:\r\n{{{\r\n{-# LANGUAGE ConstraintKinds, ImplicitParams #-}\r\nmodule Foo where\r\ntype Foo = ?foo::()\r\n}}}\r\ngives\r\n{{{\r\nFoo.hs:3:1: error:\r\n • Illegal implicit parameter ‘?foo::()’\r\n • In the type synonym declaration for ‘Foo’\r\n}}}\r\nin GHC HEAD. It used to work in GHC-7.10. Did not check GHC-8.0.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11471Kind polymorphism and unboxed types: bad things are happening2019-07-07T18:30:16ZBen GamariKind polymorphism and unboxed types: bad things are happeningThis Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---...This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Task |
| 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":"Note [The kind invariant] in TyCoRep needs to be updated","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11474incorrect redundant-constraints warning2019-07-07T18:30:15ZHerbert Valerio Riedelhvr@gnu.orgincorrect redundant-constraints warningThe following code when compiled with GHC 8
```hs
{-# LANGUAGE Haskell2010, FunctionalDependencies, KindSignatures,
ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
import GHC.Generics
data Options
data Value
...The following code when compiled with GHC 8
```hs
{-# LANGUAGE Haskell2010, FunctionalDependencies, KindSignatures,
ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
import GHC.Generics
data Options
data Value
newtype Tagged s b = Tagged {unTagged :: b}
class GToJSON f where
gToJSON :: Options -> f a -> Value
class SumToJSON f allNullary where
sumToJSON :: Options -> f a -> Tagged allNullary Value
class AllNullary (f :: * -> *) allNullary | f -> allNullary
instance (
AllNullary (a :+: b) allNullary, -- <- removing this line causes a compile error
SumToJSON (a :+: b) allNullary )
=> GToJSON (a :+: b) where
gToJSON opts = (unTagged :: Tagged allNullary Value -> Value) . sumToJSON opts
```
emits a warning
```
bug.hs:19:10: warning:
• Redundant constraint: AllNullary (a :+: b) allNullary
• In the instance declaration for ‘GToJSON (a :+: b)’
```
when commenting out the `AllNullary` constraint, this however results the compile error
```
bug.hs:19:10: error:
• Could not deduce (SumToJSON (a :+: b) allNullary0)
from the context: SumToJSON (a :+: b) allNullary
bound by an instance declaration:
SumToJSON (a :+: b) allNullary => GToJSON (a :+: b)
at redconstr.hs:(19,10)-(22,24)
The type variable ‘allNullary0’ is ambiguous
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘GToJSON (a :+: b)’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"incorrect redundant-constraints warning","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code when compiled with GHC 8\r\n\r\n{{{#!hs\r\n{-# LANGUAGE Haskell2010, FunctionalDependencies, KindSignatures,\r\n ScopedTypeVariables, TypeOperators, UndecidableInstances #-}\r\n\r\nimport GHC.Generics\r\n\r\ndata Options\r\ndata Value\r\n\r\nnewtype Tagged s b = Tagged {unTagged :: b}\r\n\r\nclass GToJSON f where\r\n gToJSON :: Options -> f a -> Value\r\n\r\nclass SumToJSON f allNullary where\r\n sumToJSON :: Options -> f a -> Tagged allNullary Value\r\n\r\nclass AllNullary (f :: * -> *) allNullary | f -> allNullary\r\n\r\ninstance (\r\n AllNullary (a :+: b) allNullary, -- <- removing this line causes a compile error\r\n SumToJSON (a :+: b) allNullary )\r\n => GToJSON (a :+: b) where\r\n\r\n gToJSON opts = (unTagged :: Tagged allNullary Value -> Value) . sumToJSON opts\r\n}}}\r\n\r\nemits a warning\r\n\r\n{{{\r\nbug.hs:19:10: warning:\r\n • Redundant constraint: AllNullary (a :+: b) allNullary\r\n • In the instance declaration for ‘GToJSON (a :+: b)’\r\n}}}\r\n\r\nwhen commenting out the `AllNullary` constraint, this however results the compile error\r\n\r\n{{{\r\nbug.hs:19:10: error:\r\n • Could not deduce (SumToJSON (a :+: b) allNullary0)\r\n from the context: SumToJSON (a :+: b) allNullary\r\n bound by an instance declaration:\r\n SumToJSON (a :+: b) allNullary => GToJSON (a :+: b)\r\n at redconstr.hs:(19,10)-(22,24)\r\n The type variable ‘allNullary0’ is ambiguous\r\n • In the ambiguity check for an instance declaration\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the instance declaration for ‘GToJSON (a :+: b)’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/11480UndecidableSuperClasses causes the compiler to spin with UndecidableInstances2019-07-07T18:30:14ZEdward KmettUndecidableSuperClasses causes the compiler to spin with UndecidableInstancesLooks like I spoke too soon when I said all my examples worked in #10318 -- it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I to...Looks like I spoke too soon when I said all my examples worked in #10318 -- it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:
```hs
{-# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances,
FunctionalDependencies, UndecidableSuperClasses #-}
import GHC.Types (Constraint)
import qualified Prelude
data Nat (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) (g :: i -> j)
class Functor p (Nat p (->)) p => Category (p :: i -> i -> *)
class (Category dom, Category cod) => Functor (dom :: i -> i -> *) (cod :: j -> j -> *) (f :: i -> j) | f -> dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (->)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (->) (Nat c d f)
instance Category (->)
instance Functor (->) (->) ((->) e)
instance Functor (->) (Nat (->) (->)) (->)
```
Sorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.
One potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.
Also, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the "real" version of the problem.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| 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":"UndecidableSuperClasses causes the compiler to spin with UndecidableInstances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["PolyKinds,","UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Looks like I spoke too soon when I said all my examples worked in #10318 -- it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.\r\n\r\nI took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:\r\n\r\n{{{#!hs\r\n{-# language KindSignatures, PolyKinds, TypeFamilies, \r\n NoImplicitPrelude, FlexibleContexts,\r\n MultiParamTypeClasses, GADTs, \r\n ConstraintKinds, FlexibleInstances, \r\n FunctionalDependencies, UndecidableSuperClasses #-}\r\n\r\nimport GHC.Types (Constraint)\r\nimport qualified Prelude\r\n\r\ndata Nat (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) (g :: i -> j)\r\n\r\nclass Functor p (Nat p (->)) p => Category (p :: i -> i -> *)\r\nclass (Category dom, Category cod) => Functor (dom :: i -> i -> *) (cod :: j -> j -> *) (f :: i -> j) | f -> dom cod\r\n\r\ninstance (Category c, Category d) => Category (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (->)) (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (->) (Nat c d f)\r\n\r\ninstance Category (->)\r\ninstance Functor (->) (->) ((->) e)\r\ninstance Functor (->) (Nat (->) (->)) (->)\r\n}}}\r\n\r\nSorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.\r\n\r\nOne potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.\r\n\r\nAlso, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the \"real\" version of the problem.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11485Very unhelpful message resulting from kind mismatch2019-07-07T18:30:13ZRyan ScottVery unhelpful message resulting from kind mismatchThe following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not e...The following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.
On GHC 7.10.3:
```
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:9:19:
Couldn't match kind ‘* -> *’ with ‘*’
Expected type: Proxy a0
Actual type: Proxy []
In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
But on GHC 8.0.1-rc1:
```
Foo.hs:9:19: error:
• Expected kind ‘Proxy []’,
but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’
• In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Very unhelpful message resulting from kind mismatch","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Data.Typeable\r\n\r\ntyConOf :: Typeable a => Proxy a -> TyCon\r\ntyConOf = typeRepTyCon . typeRep\r\n\r\ntcList :: TyCon\r\ntcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nfails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.\r\n\r\nOn GHC 7.10.3:\r\n\r\n{{{\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:9:19:\r\n Couldn't match kind ‘* -> *’ with ‘*’\r\n Expected type: Proxy a0\r\n Actual type: Proxy []\r\n In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’\r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nBut on GHC 8.0.1-rc1:\r\n\r\n{{{\r\nFoo.hs:9:19: error: \r\n • Expected kind ‘Proxy []’, \r\n but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’ \r\n • In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’ \r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11511Type family producing infinite type accepted as injective2019-07-07T18:30:07ZJan Stolarekjan.stolarek@ed.ac.ukType family producing infinite type accepted as injectiveA question came up during discussion at University of Wrocław:
```hs
type family F a = r | r -> a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool`...A question came up during discussion at University of Wrocław:
```hs
type family F a = r | r -> a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.
This is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family producing infinite type accepted as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"Bug","description":"A question came up during discussion at University of Wrocław:\r\n\r\n\r\n{{{#!hs\r\ntype family F a = r | r -> a where\r\n F a = [F a]\r\n}}}\r\n\r\nShould this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.\r\n\r\nThis is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11516Panic, "falls into a hole"2019-07-07T18:30:06ZIcelandjackPanic, "falls into a hole"```hs
{-# language PolyKinds #-}
{-# language FlexibleContexts #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
import GHC.Types (Constraint)
class Ríki (p :: i -> i -> *)
...```hs
{-# language PolyKinds #-}
{-# language FlexibleContexts #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
import GHC.Types (Constraint)
class Ríki (p :: i -> i -> *)
class (Ríki p) => Varpi p q f | f -> p q
instance Varpi () () f => Varpi (->) (->) (Either f) where
```
causes
```
% ghci -ignore-dot-ghci /tmp/testing.hs
GHCi, version 8.1.20160117: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/testing.hs, interpreted )
/tmp/testing.hs:11:10: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.1.20160117 for x86_64-unknown-linux):
fvProv falls into a hole {a13R}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
Leaving GHCi.
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.3 |
| 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":"Panic, \"falls into a hole\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# language PolyKinds #-}\r\n{-# language FlexibleContexts #-}\r\n{-# language ConstraintKinds #-}\r\n{-# language FlexibleInstances #-}\r\n{-# language FunctionalDependencies #-}\r\n\r\nimport GHC.Types (Constraint)\r\n\r\nclass Ríki (p :: i -> i -> *)\r\nclass (Ríki p) => Varpi p q f | f -> p q\r\ninstance Varpi () () f => Varpi (->) (->) (Either f) where\r\n}}}\r\n\r\ncauses\r\n\r\n{{{\r\n% ghci -ignore-dot-ghci /tmp/testing.hs \r\nGHCi, version 8.1.20160117: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/testing.hs, interpreted )\r\n\r\n/tmp/testing.hs:11:10: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160117 for x86_64-unknown-linux):\r\n fvProv falls into a hole {a13R}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\nLeaving GHCi.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2