data EType = EInt | EReal | ECVec | ERVec | EMat | EArray Nat EType

data UExprF :: EType -> Type where
  DeclareE :: StanType t -> IndexVec t -> UExprF t
  NamedE :: Text -> SType t -> UExprF t
  IntE :: Int -> UExprF EInt
  RealE :: Double -> UExprF EReal
  BinaryOpE :: SBinaryOp op -> UExprF ta -> UExprF tb -> UExprF (BinaryResultT op ta tb)
  SliceE :: SNat n -> UExprF EInt -> UExprF t -> UExprF (Sliced n t)
  NamedIndexE :: SME.IndexKey -> UExprF EInt

-- recursive version?? But not of kind (Type -> Type) -> Type -> Type ...
data UExprF1 :: (EType -> Type) -> EType -> Type where
  DeclareE :: StanType t -> IndexVec r t -> UExprF r t
  NamedE :: Text -> SType t -> UExprF r t
  IntE :: Int -> UExprF r EInt
  RealE :: Double -> UExprF r EReal
  BinaryOpE :: SBinaryOp op -> r ta -> r tb -> UExprF r (BinaryResultT op ta tb)
  SliceE :: SNat n -> r EInt -> r t -> UExprF r (Sliced n t)
  NamedIndexE :: SME.IndexKey -> UExprF r EInt