Allow Well-Founded Recursion in Data Type Kinds
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.