Model nested data stucture with 'can contain' constraint

Question

Given a set of A, B, C, D... where A contains an ordered list of As, Bs, Cs, ... and Bs have a list of Bs, Cs, Ds... and so on such that any given element can't contain any instances of a 'higher' type how would you model this?

data Hier a = A [a] | B [a] | C [a] | D [a] 

allows this nesting but won't prevent putting a A into a B.

data A = A [ACont]
data B = B [BCont]
data C = C [CCont]
data D = D

data ACont = AA A | AB B | AC C | AD D
data BCont =        BB B | BC C | BD D
data CCont =               CC C | CD D

pattern PatAA x <- AA (A x) where
   PatAA x = AA (A x)

get the nesting right but... yuck. Seven types, a zoo of constructors, no obvious functor instance, and then generically traversing this structure won't be fun. You can reduce the pain a little with some pattern synonyms (one show), but not a heck of a lot.

Is this the best that can be done?

Answer 1

(There is an answer to a similar question here)

You can do it with some type-level constraints:

data Nat = Z | S Nat

class (<=) (n :: Nat) (m :: Nat) where isLte :: n <=! m
  
instance Z <= n where isLte = LTEZ
instance n <= m => S n <= S m where isLte = LTES isLte

data (<=!) (n :: Nat) (m :: Nat) where
  LTEZ :: Z <=! n
  LTES :: n <=! m -> S n <=! S m

This code creates a class for (peano) numbers which are less than or equal to each other, and a type representing a proof of that fact.

Here's how you'd use it to make your constructors:

newtype Root (n :: Nat) = Root { getRoot :: [Branch n] }

data Branch (n :: Nat) where
  Branch :: m <= n => Root m -> Branch n
  
type A = Root (S (S (S Z)))
type B = Root (S (S Z))
type C = Root (S Z)
type D = Root Z

a :: [Branch (S (S (S Z)))] -> A
a = Root

b :: [Branch (S (S Z))] -> B
b = Root

c :: [Branch (S Z)] -> C
c = Root

d :: [Branch Z] -> D
d = Root

You can see that this gives you the right constraints, i.e.:

c [Branch (d [])] -- Passes
c [Branch (c [])] -- Passes
c [Branch (b [])] -- Fails typechecker