Using type-inequality within type-level programming in Haskell

Question

I am trying to do some advanced type-level programming; the example is a reduced version of my original program.

I have a representation of (Haskell) types. In this example I only cover function types, basic types and type variables.

The representation Type t is parameterized by one type variable t to also allow a differentiation on the type-level. To achieve this, I am mainly using GADTs. Different types and type variables are differentiated by using type-level literals, thus the KnownSymbol constraint and the use of Proxys.

{-# LANGUAGE GADTs, TypeOperators, DataKinds, KindSignatures, TypeFamilies, PolyKinds #-}

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality

data Type :: TypeKind -> * where
  TypeFun    :: Type a -> Type b -> Type (a :-> b)
  Type       :: KnownSymbol t => Proxy t -> Type (Ty t)
  TypeVar    :: KnownSymbol t => Proxy t -> Type (TyVar t)

I have also restricted the kind of t to be of kind TypeKind by using the DataKinds and KindSignatures extensions and defining the TypeKind data-type:

data TypeKind =
    Ty Symbol
  | TyVar Symbol
  | (:->) TypeKind TypeKind

Now I want to implement substitutions of type variables, i.e. substituting, within a type t, every variable x that is equal to a type variable y, with type t'. The substitution must be implemented on the representation, as well as on the type-level. For the latter, we need TypeFamilies:

type family Subst (t :: TypeKind) (y :: Symbol) (t' :: TypeKind) :: TypeKind where
  Subst (Ty t) y t'    = Ty t
  Subst (a :-> b) y t' = Subst a y t' :-> Subst b y t'
  Subst (TyVar x) y t' = IfThenElse (x == y) t' (TyVar x)

The type variables are the interesting part, because we check for the equality of the symbols x and y on the type-level. For this, we also need a (poly-kinded) type family that allows us to choose between two results:

type family IfThenElse (b :: Bool) (x :: k) (y :: k) :: k where
  IfThenElse True  x y = x
  IfThenElse False x y = y

Unfortunately, this does not compile yet, which might be the first indicator of my problem:

Nested type family application
  in the type family application: IfThenElse (x == y) t' ('TyVar x)
(Use UndecidableInstances to permit this)
In the equations for closed type family ‘Subst’
In the type family declaration for ‘Subst’

Enabling the UndecidableInstances extension works, though, so we continue to define a function subst that works on the value-level:

subst :: (KnownSymbol y) => Type t -> Proxy (y :: Symbol) -> Type t' -> Type (Subst t y t')
subst (TypeFun a b) y t = TypeFun (subst a y t) (subst b y t)
subst t@(Type _) _ _    = t
subst t@(TypeVar x) y t'
  | Just Refl <- sameSymbol x y = t'
  | otherwise                   = t

This code works perfectly, except for the last line which produces the following compilation error:

Could not deduce (IfThenElse
                    (GHC.TypeLits.EqSymbol t1 y) t' ('TyVar t1)
                  ~ 'TyVar t1)
from the context (t ~ 'TyVar t1, KnownSymbol t1)
  bound by a pattern with constructor
             TypeVar :: forall (t :: Symbol).
                        KnownSymbol t =>
                        Proxy t -> Type ('TyVar t),
           in an equation for ‘subst’
  at Type.hs:29:10-18
Expected type: Type (Subst t y t')
  Actual type: Type t
Relevant bindings include
  t' :: Type t' (bound at Type.hs:29:23)
  y :: Proxy y (bound at Type.hs:29:21)
  x :: Proxy t1 (bound at Type.hs:29:18)
  subst :: Type t -> Proxy y -> Type t' -> Type (Subst t y t')
    (bound at Type.hs:27:1)
In the expression: t
In an equation for ‘subst’:
    subst t@(TypeVar x) y t'
      | Just Refl <- sameSymbol x y = t'
      | otherwise = t

I guess that the problem is that I cannot prove the inequality of the types of the two symbols x and y, and would need some kind of type-inequality witness. Is this possible? Or is there another, better way to achieve my goal? I do not know to which extent the questions 'idiomatic' Haskell type inequality and Can GADTs be used to prove type inequalities in GHC? already answer my question. Any help would be appreciated.

Answer 1

As chi said in the comments, what you need is Either ((x==y) :~: True) ((x==y) :~: False). Unfortunately, type literals are partly broken currently, and this is one of the things we can only do with unsafeCoerce (a morally acceptable use though).

sameSymbol' ::
  (KnownSymbol s, KnownSymbol s') =>
  Proxy s -> Proxy s'
  -> Either ((s == s') :~: True) ((s == s') :~: False)
sameSymbol' s s' = case sameSymbol s s' of
  Just Refl -> Left Refl
  Nothing   -> Right (unsafeCoerce Refl)

subst :: (KnownSymbol y) => Type t -> Proxy (y :: Symbol) -> Type t' -> Type (Subst t y t')
subst (TypeFun a b) y t = TypeFun (subst a y t) (subst b y t)
subst t@(Type _) _ _    = t
subst t@(TypeVar x) y t' = case sameSymbol' x y of
  Left  Refl -> t'
  Right Refl -> t

On another note, if you don't mind some Template Haskell, the singletons library can derive your definitions (and more):

{-# language GADTs, TypeOperators, DataKinds, KindSignatures, TypeFamilies, PolyKinds #-}
{-# language UndecidableInstances, ScopedTypeVariables, TemplateHaskell, FlexibleContexts #-}

import GHC.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude

singletons([d|
  data Type sym
    = Ty sym
    | TyVar sym
    | Type sym :-> Type sym

  subst :: Eq sym => Type sym -> sym -> Type sym -> Type sym
  subst (Ty t) y t'    = Ty t
  subst (a :-> b) y t' = subst a y t' :-> subst b y t'
  subst (TyVar x) y t' = if x == y then t' else TyVar x        
  |])

This gives us type, kind and value level definitions for Type and subst. Examples:

-- some examples

-- type level
type T1 = Ty "a" :-> TyVar "b"
type T2 = Subst T1 "b" (Ty "c") -- this equals (Ty "a" :-> Ty "c")

-- value level

-- automatically create value-level representation of T1
t1  = sing :: Sing T1

-- or write it out by hand
t1' = STy (sing :: Sing "a") :%-> STyVar (sing :: Sing "b")

-- use value-level subst on t1:
t2 = sSubst t1 (sing :: Sing "b") (STy (sing :: Sing "c"))

-- or generate result from type-level representation
t2' = sing :: Sing (Subst T1 "b" (Ty "c"))

-- Convert singleton to non-singleton (and print it)
t3 :: Type String
t3 = fromSing t2 -- Ty "a" :-> Ty "c"