How to coerce types from different type levels in Haskell?

Question

I have the following code:

type Name = String

data Level = T0 | T1 | T2

data T (l :: Level) where
    Tint  :: T t
    Tdyn  :: T t
    Tbool :: T t
    Tarr  :: T 'T0 -> T 'T0 -> T t
    Tand  :: T 'T1 -> T 'T1 -> T 'T1
    Tarr2 :: T 'T1 -> T 'T2 -> T 'T2


class Arr (l1 :: Level) (l2 :: Level) (l3 :: Level) | l3 -> l1 l2 where
    infixr 3 ~>
    (~>) :: T l1 -> T l2 -> T l3

instance Arr 'T0 'T0 'T0 where 
    (~>) = Tarr 

instance Arr 'T0 'T0 'T1 where 
    (~>) = Tarr 

instance Arr 'T1 'T2 'T2 where
    (~>) = Tarr2

infixr 5 /\
(/\) :: T 'T1 -> T 'T1 -> T 'T1
(/\) = Tand

infixr 3 ~.>
(~.>) :: T 'T0 -> T 'T0 -> T t
(~.>) = Tarr

infixr 3 ~!>
(~!>) :: T 'T1 -> T 'T2 -> T 'T2
(~!>) = Tarr2

type Typ2 = T 'T2
type Typ1 = T 'T1
type Typ0 = T 'T0

int :: T t 
int = Tint

bool :: T t 
bool = Tbool

dyn :: T t
dyn = Tdyn

newType :: Typ2
newType = int /\ int ~> int /\ int ~> dyn



data Expr = Vi Int
          | Vb Bool
          | Vv Name
          | App Expr Expr
          | Lam Name Typ1 Expr
          deriving(Generic)

type Env = [(Name,Typ1)]

Basically, I have three kinds of types. T0, T1 and T2. Note that T0 is also a T1 and T0 is also a T2.

I would like to write a type-checker though with the following signature:

typecheck :: Expr -> Env -> [Typ2]

It needs to call a function with this signature:

Name -> Env ->  [Typ0]

The issue is that I cannot be returning a [Typ0] as a [Typ2] according to the compiler, so I am assuming I need to do coersions?

Does anyone know what's the best thing to do in this situation?

Edit:

typecheck :: Expr -> Env -> [Typ2]
typecheck (Vv x) env = (envlookup x env)


envlookup :: Name -> Env ->  [Typ0]
envlookup name = 
    \case 
    (n,t):xs
        | n == name -> 
        case t of 
            int -> [int]
            -- otherwise -> t 
    [] -> []

Answer 1

One option is to write a function which raises the level of a type:

raise0 :: T T0 -> T t
raise0 Tint = Tint
raise0 Tdyn = Tdyn
raise0 Tbool = Tbool
raise0 (Tarr i e) = Tarr i e

In particular, this can be used at the type Typ0 -> Typ2. Another would be to make your environment types take the level as an argument:

envlookup :: Name -> Env t -> [T t]
envlookup name env = [t | (n, t) <- env, n == name]

A third alternative would be to ensure that the types in environments can be used at any level:

newtype AnyT = AnyT (forall t. T t)
type Env = [(Name, AnyT)]

envlookup :: Name -> Env -> [T t]
envlookup name env = [t | (n, AnyT t) <- env, n == name]