GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-02-18T12:30:12Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16877GHCi panics using -fdefer-type-errors when pattern matching on types with mul...2020-02-18T12:30:12ZBerengalGHCi panics using -fdefer-type-errors when pattern matching on types with multiple constructors using out-of-scope variables# Summary
With -fdefer-type-errors enabled GHCi will panic on certain errors involving pattern matching on types with multiple constructors. At least as far as I can tell.
# Steps to reproduce
The following is the smallest module I co...# Summary
With -fdefer-type-errors enabled GHCi will panic on certain errors involving pattern matching on types with multiple constructors. At least as far as I can tell.
# Steps to reproduce
The following is the smallest module I could find that causes the panic:
```
foo = x
where (x:xs) = bar
```
GHCi command and output:
```
▶ ghci -ignore-dot-ghci -fdefer-type-errors Foo.hs
GHCi, version 8.6.5: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:2:18: warning: [-Wdeferred-out-of-scope-variables]
Variable not in scope: bar :: [a1]
|
2 | where (x:xs) = bar
| ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64-unknown-linux):
getIdFromTrivialExpr
\ (@ a_a1x4) -> case ds_s1yU @ a_a1x4 of wild_Xb { }
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/coreSyn/CoreUtils.hs:977:18 in ghc:CoreUtils
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
The equivalent using `let` also panics. The pattern match in the where is neccessary, as is using a matched variable in the main expression (either one will do). Matching on a tuple does not cause a panic, nor does matching on `data Foo a = Foo a a`, but matching on `data Foo a = Foo a a | Bar a a` panics regardless of which constructor is chosen.
# Expected behavior
GHCi doesn't panic, but either loads the module correctly or explains why it can't do so.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Arch-linux
* System Architecture: x86_648.8.2https://gitlab.haskell.org/ghc/ghc/-/issues/16775Don't zap naughty quantification candidates: error instead2020-12-15T12:32:56ZRichard Eisenbergrae@richarde.devDon't zap naughty quantification candidates: error insteadNote [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we sim...Note [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`-ify in type declarations. And I think we are wrong to `Any`-ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partial-sigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locally-bound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a -> Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k -> *’, but ‘f’ has kind ‘k -> Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a -> Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a -> Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a -> Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
|
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
| ^
Scratch.hs:44:63: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((->) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:1-9
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’
|
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
| ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?8.8.2https://gitlab.haskell.org/ghc/ghc/-/issues/15577TypeApplications-related infinite loop (GHC 8.6+ only)2019-08-30T12:55:21ZRyan ScottTypeApplications-related infinite loop (GHC 8.6+ only)The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Ty...The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k -> Type
class Generic1 (f :: k -> Type) where
type Rep1 f :: k -> Type
class PGeneric1 (f :: k -> Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k -> Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r -> From1 (To1 r :: f a) :~: r
foo x
| Refl <- sFot1 -- Uncommenting the line below makes it work again:
-- @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* -> *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
|
35 | @f @a @r x
| ^
Bug.hs:35:23: error:
• Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl <- sFot1 @f @a @r x
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
35 | @f @a @r x
| ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:5-8
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 -> From1 (To1 r1) :~: r1
at Bug.hs:(29,1)-(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)
|
36 | = Refl
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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":"TypeApplications-related infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k -> Type\r\n\r\nclass Generic1 (f :: k -> Type) where\r\n type Rep1 f :: k -> Type\r\n\r\nclass PGeneric1 (f :: k -> Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k -> Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r -> From1 (To1 r :: f a) :~: r\r\nfoo x\r\n | Refl <- sFot1 -- Uncommenting the line below makes it work again:\r\n -- @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* -> *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* -> *’ with ‘*’\r\n When matching kinds\r\n f1 :: * -> *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl <- sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n35 | @f @a @r x\r\n | ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:5-8\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 -> From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)-(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n |\r\n36 | = Refl\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.2Ben GamariAlp MestanogullariBen Gamari