Skip to content

Matchability inference bugs

The following panics:

type Poly :: forall m. Nat -> (Type -> @m Type) -> Type
type family Poly n (f :: Type -> @m Type) where
  Poly 0 m = m Int
  Poly 1 f = f (Poly 0 Maybe)
  Poly n f = f (Poly (n - 1) Id)
ghc: panic! (the 'impossible' happened)
  (GHC version 8.11.0.20200829:
        ASSERT failed!
  3
  1
  m_a127[tyv:1:In type family:TvNone:False]
  m_a11O[sk:3]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Panic.hs:185:37 in ghc:GHC.Utils.Panic
        pprPanic, called at compiler/GHC/Utils/Panic.hs:304:5 in ghc:GHC.Utils.Panic
        assertPprPanic, called at compiler/GHC/Tc/Utils/TcMType.hs:1005:54 in ghc:GHC.Tc.Utils.TcMType

and this one fails:

type Poly :: forall m. Nat -> (Type -> @m Type) -> Type
type family Poly n f where
  Poly 0 m = m Int
  Poly 1 f = f (Poly 0 Maybe)
  Poly n f = f (Poly (n - 1) Id)
SAKS11.hs:21:3: error:
    • Number of parameters must match family declaration; expected 1
    • In the type family declaration for ‘Poly’
   |
21 |   Poly 0 m = m Int
   |   ^^^^^^^^^^^^^^^^

SAKS11.hs:22:3: error:
    • Number of parameters must match family declaration; expected 1
    • In the type family declaration for ‘Poly’
   |
22 |   Poly 1 f = f (Poly 0 Maybe)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

SAKS11.hs:23:3: error:
    • Number of parameters must match family declaration; expected 1
    • In the type family declaration for ‘Poly’
   |
23 |   Poly n f = f (Poly (n - 1) Id)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^