{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

module Repr where

import TEq
import Base

-- * Operations on type representations

class Repr s where
  ixeq :: Monad m => s ix -> s ix' -> m (ix :=: ix')

coerce :: (Repr s, Monad m) => s ix -> s ix' -> f ix -> m (f ix')
coerce ix ix' x =
  do
    Refl <- ixeq ix ix'
    return x