{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
import GHC.TypeNats

data Note (num :: Nat) (denom :: Nat) where
  Whole :: Note denom denom
  Half :: Note num denom -> Note num (2 * denom)
  Triplet :: Note num denom -> Note num (3 * denom)

data Sequence (num :: Nat) (denom :: Nat) where
  Nil :: Sequence 0 denom
  Cons :: Note num denom -> Sequence num' denom -> Sequence (num + num') denom
infixr 5 `Cons`

data Measure where
  Measure :: Sequence len len -> Measure

m = Measure @6 $
  Triplet Whole `Cons`
  Half Whole `Cons`
  Triplet (Half Whole) `Cons` Nil

main = pure ()