{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Array.Nested.Internal where

import Data.Coerce (coerce)


type family Id (b :: Bool) where
  Id b = b

newtype Ranked b a = MkRanked (Mixed b a)


data family Mixed (b :: Bool) a

newtype instance Mixed b1 (Mixed b2 a) = M_Nest (Mixed False a)

newtype instance Mixed b (Ranked c a) = M_Ranked (Mixed b (Mixed (Id c) a))


idMixed :: Mixed b a -> Mixed b a
idMixed = undefined

bar :: Mixed b (Ranked c a) -> Mixed b (Ranked c a)
bar (M_Ranked @_ @c @a arr)
  = coerce (idMixed arr)                          -- fails
  -- = coerce (idMixed @_ @(Mixed (Id c) a) arr)  -- ok
  -- = coerce (id arr)                            -- ok
  -- = let r = idMixed arr in coerce r            -- ok