GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-04-07T15:59:29Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17977Coverage checker throws "tyOracle" panic on 8.10.1 or later2021-04-07T15:59:29ZRyan ScottCoverage checker throws "tyOracle" panic on 8.10.1 or laterUsing this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomp...Using this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns -Woverlapping-patterns #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data Nat = Z | S Nat
data SNat :: Nat -> Type where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family S' (n :: Nat) :: Nat where
S' n = S n
data R :: Nat -> Nat -> Nat -> Type where
MkR :: !(R m n o) -> R (S m) n (S o)
type family NatPlus (m :: Nat) (n :: Nat) :: Nat where
NatPlus Z n = n
NatPlus (S m) n = S' (NatPlus m n)
f :: forall (m :: Nat) (n :: Nat) (o :: Nat).
SNat m -> SNat n -> SNat o
-> R m n o -> NatPlus m n :~: o
f (SS sm) sn (SS so) (MkR r)
| Refl <- f sm sn so r
= Refl
```
Compiling with GHC 8.8.3 simply results in a non-exhaustivity warning, as expected:
```
$ /opt/ghc/8.8.3/bin/ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:32:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for âfâ:
Patterns not matched:
SZ _ _ _
(SS _) _ SZ _
|
32 | f (SS sm) sn (SS so) (MkR r)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
Compiling with 8.10.1 or HEAD, however, throws a GHC panic:
```
$ /opt/ghc/8.10.1/bin/ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.1:
tyOracle
Bug.hs:32:1: error:
Reduction stack overflow; size = 201
When simplifying the following type: Bug.S' (Bug.NatPlus m n)
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/GHC/HsToCore/PmCheck/Oracle.hs:526:27 in ghc:GHC.HsToCore.PmCheck.Oracle
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
As the panic suggests, compiling with `-freduction-depth=0` makes the issue go away, so perhaps this error is warranted. GHC ought to communicate this information in a friendlier way, however, since a GHC panic should not occur unless something has gone terribly wrong.8.10.2Sebastian GrafSebastian Graf