Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information