GitLab

GHC does not accept this program:

type Nat :: Type
data Nat = S Nat | Z

type Supertype :: Nat -> Type
data Supertype :: Nat -> Type where
  SupertypeNext :: forall (n :: Nat) (super :: Supertype n). Ty n super -> Supertype ('S n)
  SupertypeDone :: Supertype 'Z

type Ty :: forall (n :: Nat) -> Supertype n -> Type
data Ty :: forall (n :: Nat) -> Supertype n -> Type where
  Cons :: Ty ('S 'Z) ('SupertypeNext 'List)
  Nil :: Ty ('S 'Z) ('SupertypeNext 'List)
  List :: Ty 'Z 'SupertypeDone

GHC rejects the program with:

    • Type constructor ‘Supertype’ cannot be used here
        (it is defined and used in the same recursive group)
    • In a standalone kind signature for ‘Ty’:
        forall (n :: Nat) -> Supertype n -> Type
   |
93 | type Ty :: forall (n :: Nat) -> Supertype n -> Type
   |                                 ^^^^^^^^^^^

Agda does accept its equivalent of this program:

data Nat : Set where
  S : Nat -> Nat
  Z : Nat

mutual
  data Supertype : Nat -> Set where
    SupertypeNext : (n : Nat) -> (super : Supertype n) -> Ty n super -> Supertype (S n)
    SupertypeDone : Supertype Z

  data Ty : (n : Nat) -> Supertype n -> Set where
    List : Ty Z SupertypeDone
    Cons : Ty (S Z) (SupertypeNext Z SupertypeDone List)
    Nil : Ty (S Z) (SupertypeNext Z SupertypeDone List)

I am not sure if this is the same thing as induction recursion or not. That feature is discussed at #11962, but the example uses type families instead. The same issue may lie at the heart of both of these. Here, Supertype's data constructors do not actually reference any of Ty's data constructors, but Ty's data constructors do reference Supertype's data constructors.