Coverage checker throws "tyOracle" panic on 8.10.1 or later
Using this program:
{-# 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.