What's the effect of imposing the following restriction on inductive type families?

Question

Let a simple expression be either:

• A free variable
• A data constructor of an inductive type family, applied to 0 or more simple expressions

What would be the effect of imposing the following restriction on a programming language with inductive type families?

Given a data constructor C of an inductive type family T, within C's type signature, T and (=) (the propositional equality type constructor) may only appear fully applied to simple expressions whose free variables are bound within the type signature itself.

For example, in GHC Haskell (to avoid writing foralls in obvious places):

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Color = Red | Black
data Sign = Positive | Negative

-- Bad: Test appears applied to Color and Sign, neither
-- of which is a data constructor of an inductive type.
data Test :: * -> * where
  Foo :: Integer -> Test Color
  Bar :: Float   -> Test Sign

-- Good: List only appears applied to free variables.
data List :: (k -> k -> *) -> k -> k -> * where
  Nil  ::                        List f a a
  Cons :: f a b -> List f b c -> List f a c

-- Good: RBT appears applied to Black and Red, both of
-- which are constructors of an inductive type (Color).
data RBT :: Color -> * -> * where
  Empty ::                                    RBT Black a
  R     :: RBT Black a -> a -> RBT Black a -> RBT Red   a
  B     :: RBT l     a -> a -> RBT r     a -> RBT Black a

Now, what I want to know is:

1. From the POV of language implementors, can this restriction simplify type checking? How much?

2. From the POV of programmers using languages like Agda, Idris, Coq, etc., are there any useful programs that type check without the restriction, that can't be refactored into equivalent programs that type check under the restriction?

3. From the POV of type theorists and other mathematicians using type theory as a foundational system, does the restriction prevent any useful mathematical results from being obtained internally to type theory?

Answer 1

This is not a real restriction to the power of the language

First, it is possible to turn all indices of the type family into variables by adding extra arguments to the constructor expressing the constraints. For example, Test can be turned into

data Test a where Foo :: Integer -> a = Color -> Test a Bar :: Float -> a = Sign -> Test a

Second, you can define your own version of the propositional equality as an inductive family and use that instead of the built-in one.

data Eq :: * -> * -> * where Refl :: Eq a a

This definition follows your restrictions, but it won't be detected as being 'the' identity type. (In case you want to build in some kind of detection for identity-like types, I'd guess that the property of being identity-like may well be undecidable.) So there is nothing that you can do without your restriction that you couldn't do with it in a (somewhat) more complicated way.