Is it possible to ensure that two GADT type variables are the same without dependent types?

Question

I'm writing a compiler where I'm using GADTs for my IR but standard data types for my everything else. I'm having trouble during the conversion from the old data type to the GADT. I've attempted to recreate the situation with a smaller/simplified language below.

To start with, I have the following data types:

data OldLVal = VarOL Int -- The nth variable. Can be used to construct a Temp later.
             | LDeref OldLVal

data Exp = Var Int -- See above
         | IntT Int32
         | Deref Exp

data Statement = AssignStmt OldLVal Exp
               | ...

I want to convert these into this intermediate form:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}

-- Note: this is a Phantom type
data Temp a = Temp Int

data Type = IntT
          | PtrT Type

data Command where
    Assign :: NewLVal a -> Pure a -> Command
    ...

data NewLVal :: Type -> * where
    VarNL :: Temp a -> NewLVal a
    DerefNL :: NewLVal ('PtrT ('Just a)) -> NewLVal a

data Pure :: Type -> * where
    ConstP :: Int32 -> Pure 'IntT
    ConstPtrP :: Int32 -> Pure ('PtrT a)
    VarP :: Temp a -> Pure a

At this point, I just want to write a conversion from the old data type to the new GADT. For right now, I have something that looks like this.

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
   newLval <- convertLVal oldLval -- Either String (NewLVal a)
   pure <- convertPure exp -- Either String (Pure b)
   -- return $ Assign newLval pure -- Obvious failure. Can't ensure a ~ b.
   pure' <- matchType newLval pure -- Either String (Pure a)
   return $ Assign newLval pure'

-- Converts Pure b into Pure a. Should essentially be a noop, but simply 
-- proves that it is possible.
matchType :: NewLVal a -> Pure b -> Either String (Pure a)
matchType = undefined

I realized that I couldn't write convert trivially, so I attempted to solve the problem using this idea of matchType which acts as a proof that these two types are indeed equal. The question is: how do I actually write matchType? This would be much easier if I had fully dependent types (or so I'm told), but can I finish this code here?

An alternative to this would be to somehow provide newLval as an argument to convertPure, but I think that essentially is just attempting to use dependent types.

Any other suggestions are welcome.

If it helps, I also have a function that can convert an Exp or OldLVal to its type:

class Typed a where
    typeOf :: a -> Type
instance Typed Exp where
    ...
instance Typed OldLVal where
    ...

EDIT:

Thanks to the excellent answers below, I've been able to finish writing this module.

I ended up using the singletons package mentioned below. It was a little strange at first, but I found it pretty reasonable to use after I started understanding what I was doing. However, I did run into one pitfall: The type of convertLVal and convertPure requires an existential to express.

data WrappedPure = forall a. WrappedPure (Pure a, SType a)
data WrappedLVal = forall a. WrappedLVal (NewLVal a, SType a)

convertPure :: Exp -> Either String WrappedPure
convertLVal :: OldLVal -> Either String WrappedLVal

This means that you'll have to unwrap that existential in convert, but otherwise, the answers below show you the way. Thanks so much once again.

Answer 1

You want to perform a comparison at runtime on some type level data (namely the Types by which your values are indexed). But by the time you run your code, and the values start to interact, the types are long gone. They're erased by the compiler, in the name of producing efficient code. So you need to manually reconstruct the type level data that was erased, using a value which reminds you of the type you'd forgotten you were looking at. You need a singleton copy of Type.

data SType t where
    SIntT :: SType IntT
    SPtrT :: SType t -> SType (PtrT t)

Members of SType look like members of Type - compare the structure of a value like SPtrT (SPtrT SIntT) with that of PtrT (PtrT IntT) - but they're indexed by the (type-level) Types that they resemble. For each t :: Type there's precisely one SType t (hence the name singleton), and because SType is a GADT, pattern matching on an SType t tells the type checker about the t. Singletons span the otherwise strictly-enforced separation between types and values.

So when you're constructing your typed tree, you need to track the runtime STypes of your values and compare them when necessary. (This basically amounts to writing a partially verified type checker.) There's a class in Data.Type.Equality containing a function which compares two singletons and tells you whether their indexes match or not.

instance TestEquality SType where
    -- testEquality :: SType t1 -> SType t2 -> Maybe (t1 :~: t2)
    testEquality SIntT SIntT = Just Refl
    testEquality (SPtrT t1) (SPtrT t2)
        | Just Refl <- testEquality t1 t2 = Just Refl
    testEquality _ _ = Nothing

Applying this in your convert function looks roughly like this:

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
    (newLval, newLValSType) <- convertLVal oldLval
    (pure, pureSType) <- convertPure exp
    case testEquality newLValSType pureSType of
        Just Refl -> return $ Assign newLval pure'
        Nothing -> Left "type mismatch"

There actually aren't a whole lot of dependently typed programs you can't fake up with TypeInType and singletons (are there any?), but it's a real hassle to duplicate all of your datatypes in both "normal" and "singleton" form. (The duplication gets even worse if you want to pass singletons around implicitly - see Hasochism for the details.) The singletons package can generate much of the boilerplate for you, but it doesn't really alleviate the pain caused by duplicating the concepts themselves. That's why people want to add real dependent types to Haskell, but we're a good few years away from that yet.

The new Type.Reflection module contains a rewritten Typeable class. Its TypeRep is GADT-like and can act as a sort of "universal singleton". But programming with it is even more awkward than programming with singletons, in my opinion.

Answer 2

matchType as written is not possible to implement, but the idea you are going for is definitely possible. Do you know about Data.Typeable? Typeable is a class that provides some basic reflective operations for inspecting types. To use it, you need a Typeable a constraint in scope for any type variable a you want to know about. So for matchType you would have

matchType :: (Typeable a, Typeable b) => NewLVal a -> Pure b -> Either String (Pure a)

It needs also to infect your GADTs any time you want to hide a type variable:

data Command where
    Assign :: (Typeable a) => NewLVal a -> Pure a -> Command
    ...

But if you have the appropriate constraints in scope, you can use eqT to make type-safe runtime type comparisons. For example

-- using ScopedTypeVariables and TypeApplications
matchType :: forall a b. (Typeable a, Typeable b) => NewLVal a -> Pure b -> Either String (Pure b)
matchType = case eqT @a @b of
                Nothing -> Left "types are not equal"
                Just Refl -> {- in this scope the compiler knows that
                                a and b are the same type -}