~jojo/Carth

2ce9da50b856dfaae81d68fe42df6f9822ad9f26 — JoJo 1 year, 10 months ago a01dca2
Move decision tree compilation of pattern matches to separate pass

This is better because the types of the AST must be fully inferred
before doing this, so unless it happens in a separate pass after
inference and substitution, we have to do "inline" substitution, which
is hacky.
7 files changed, 172 insertions(+), 144 deletions(-)

M src/AnnotAst.hs
M src/Check.hs
M src/Desugar.hs
M src/Infer.hs
M src/Match.hs
M src/Misc.hs
M src/Subst.hs
M src/AnnotAst.hs => src/AnnotAst.hs +35 -13
@@ 12,8 12,12 @@ module AnnotAst
    , VariantIx
    , Access(..)
    , Span
    , VarBindings
    , Con(..)
    , Pat'(..)
    , Pat
    , Cases(..)
    , DecisionTree(..)
    , VarBindings
    , Expr
    , Expr'(..)
    , Defs


@@ 48,29 52,47 @@ data Access

type Span = Integer

type VarBindings = Map TypedVar Access
data Con = Con
    { variant :: VariantIx
    , span :: Span
    , argTs :: [Type]
    }
    deriving Show

data Pat'
    = PVar TypedVar
    | PWild
    | PCon Con [Pat]
    | PBox Pat
    deriving Show
type Pat = WithPos Pat'

newtype Cases = Cases [(Pat, Expr Cases)]
    deriving Show

data DecisionTree
    = DLeaf (VarBindings, Expr)
    = DLeaf (VarBindings, Expr DecisionTree)
    | DSwitch Access (Map VariantIx DecisionTree) DecisionTree
    deriving Show

data Expr'
type VarBindings = Map TypedVar Access

data Expr' m
    = Lit Const
    | Var TypedVar
    | App Expr Expr Type
    | If Expr Expr Expr
    | Let Defs Expr
    | Match Expr DecisionTree Type
    | FunMatch DecisionTree Type Type
    | App (Expr m) (Expr m) Type
    | If (Expr m) (Expr m) (Expr m)
    | Let (Defs m) (Expr m)
    | Match (Expr m) m Type Type
    | FunMatch m Type Type
    | Ctor VariantIx Span TConst [Type]
    | Box Expr
    | Deref Expr
    | Box (Expr m)
    | Deref (Expr m)
    deriving (Show)

type Expr = WithPos Expr'
type Expr m = WithPos (Expr' m)

type Defs = Map String (Scheme, Expr)
type Defs m = Map String (Scheme, Expr m)
type TypeDefs = Map String ([TVar], [(String, [Type])])
type Ctors = Map String (VariantIx, (String, [TVar]), [Type], Span)
type Externs = Map String Type

M src/Check.hs => src/Check.hs +55 -25
@@ 6,13 6,16 @@ import Prelude hiding (span)
import Control.Monad.Except
import Control.Monad.Reader
import Data.Bifunctor
import Data.Bitraversable
import Data.Foldable
import Control.Applicative
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Maybe

import Misc
import SrcPos
import Subst
import qualified Ast


@@ 29,10 32,12 @@ import qualified DesugaredAst as Des
typecheck :: Ast.Program -> Either TypeErr Des.Program
typecheck (Ast.Program defs tdefs externs) = runExcept $ do
    (tdefs', ctors) <- checkTypeDefs tdefs
    (externs', inferred, substs) <- inferTopDefs tdefs' ctors externs defs
    (externs', inferred, substs) <- inferTopDefs ctors externs defs
    let substd = substTopDefs substs inferred
    checkTypeVarsBound substd
    let desugared = desugar substd
    let mTypeDefs = fmap (map fst . snd) tdefs'
    checked <- checkPatternMatches mTypeDefs substd
    let desugared = desugar checked
    let tdefs'' = fmap (second (map snd)) tdefs'
    pure (Des.Program desugared tdefs'' externs')



@@ 143,10 148,10 @@ type Bound = ReaderT (Set TVar) (Except TypeErr) ()

-- TODO: Many of these positions are weird and kind of arbitrary, man. They may
--       not align with where the type variable is actually detected.
checkTypeVarsBound :: An.Defs -> Except TypeErr ()
checkTypeVarsBound :: An.Defs An.Cases -> Except TypeErr ()
checkTypeVarsBound ds = runReaderT (boundInDefs ds) Set.empty
  where
    boundInDefs :: An.Defs -> Bound
    boundInDefs :: An.Defs An.Cases -> Bound
    boundInDefs = mapM_ boundInDef
    boundInDef ((An.Forall tvs _), e) =
        local (Set.union tvs) (boundInExpr e)


@@ 164,12 169,13 @@ checkTypeVarsBound ds = runReaderT (boundInDefs ds) Set.empty
        An.Let lds b -> do
            boundInDefs lds
            boundInExpr b
        An.Match m dt bt -> do
        An.Match m cs tp tb -> do
            boundInExpr m
            boundInDecTree dt
            boundInType pos bt
        An.FunMatch dt pt bt -> do
            boundInDecTree dt
            boundInCases cs
            boundInType pos tp
            boundInType pos tb
        An.FunMatch cs pt bt -> do
            boundInCases cs
            boundInType pos pt
            boundInType pos bt
        An.Ctor _ _ (_, instTs) ts -> do


@@ 179,23 185,47 @@ checkTypeVarsBound ds = runReaderT (boundInDefs ds) Set.empty
        An.Deref x -> boundInExpr x
    boundInType :: SrcPos -> An.Type -> Bound
    boundInType pos = \case
        TVar tv ->
            ask
                >>= \bound -> when
                        (not (Set.member tv bound))
                        (throwError (UnboundTVar pos))
        TVar tv -> do
            bound <- ask
            when (not (Set.member tv bound)) (throwError (UnboundTVar pos))
        TPrim _ -> pure ()
        TConst (_, ts) -> forM_ ts (boundInType pos)
        TFun ft at -> forM_ [ft, at] (boundInType pos)
        TBox t -> boundInType pos t
    boundInDecTree = \case
        An.DLeaf (bs, e) -> do
            forM_ (Map.toList bs) $ \(An.TypedVar (WithPos p _) t, a) ->
                boundInType p t *> boundInAccess p a
            boundInExpr e
        An.DSwitch _ dts dt -> forM_ (dt : Map.elems dts) boundInDecTree
    boundInAccess pos = \case
        Des.Obj -> pure ()
        Des.As a _ ts -> boundInAccess pos a *> forM_ ts (boundInType pos)
        Des.Sel _ _ a -> boundInAccess pos a
        Des.ADeref a -> boundInAccess pos a
    boundInCases (An.Cases cs) = forM_ cs (bimapM boundInPat boundInExpr)
    boundInPat (WithPos pos pat) = case pat of
        An.PVar (An.TypedVar _ t) -> boundInType pos t
        An.PWild -> pure ()
        An.PCon con ps -> boundInCon pos con *> forM_ ps boundInPat
        An.PBox p -> boundInPat p
    boundInCon pos (Con _ _ ts) = forM_ ts (boundInType pos)

checkPatternMatches
    :: MTypeDefs -> An.Defs An.Cases -> Except TypeErr (An.Defs An.DecisionTree)
checkPatternMatches tdefs = checkMsDefs
  where
    checkMsDefs = mapM checkMsDef
    checkMsDef = bimapM pure checkMsExpr
    checkMsExpr
        :: An.Expr An.Cases -> Except TypeErr (An.Expr An.DecisionTree)
    checkMsExpr (WithPos pos e) = fmap (WithPos pos) $ case e of
        An.Lit c -> pure (An.Lit c)
        An.Var v -> pure (An.Var v)
        An.App f a tr ->
            liftA3 An.App (checkMsExpr f) (checkMsExpr a) (pure tr)
        An.If p c a ->
            liftA3 An.If (checkMsExpr p) (checkMsExpr c) (checkMsExpr a)
        An.Let lds b -> liftA2 An.Let (checkMsDefs lds) (checkMsExpr b)
        An.Match m cs tp tb -> do
            m' <- checkMsExpr m
            dt <- toDecisionTree' pos tp cs
            pure (An.Match m' dt tp tb)
        An.FunMatch cs tp tb -> fmap
            (\dt -> An.FunMatch dt tp tb)
            (toDecisionTree' pos tp cs)
        An.Ctor v s tc ts -> pure (An.Ctor v s tc ts)
        An.Box x -> fmap An.Box (checkMsExpr x)
        An.Deref x -> fmap An.Deref (checkMsExpr x)
    toDecisionTree' pos tp (An.Cases cs) = do
        cs' <- mapM (secondM checkMsExpr) cs
        toDecisionTree tdefs pos tp cs'

M src/Desugar.hs => src/Desugar.hs +8 -4
@@ 9,20 9,24 @@ import SrcPos
import qualified AnnotAst as An
import DesugaredAst

desugar :: An.Defs -> Defs

type ADefs = An.Defs An.DecisionTree
type AExpr = An.Expr An.DecisionTree

desugar :: ADefs -> Defs
desugar = desugarDefs

desugarDefs :: An.Defs -> Defs
desugarDefs :: ADefs -> Defs
desugarDefs = fmap (second desugarExpr)

desugarExpr :: An.Expr -> Expr
desugarExpr :: AExpr -> Expr
desugarExpr (WithPos _ e) = case e of
    An.Lit c -> Lit c
    An.Var v -> Var (desugarTypedVar v)
    An.App f a rt -> App (desugarExpr f) (desugarExpr a) rt
    An.If p c a -> If (desugarExpr p) (desugarExpr c) (desugarExpr a)
    An.Let ds b -> Let (desugarDefs ds) (desugarExpr b)
    An.Match m dt t -> Match (desugarExpr m) (desugarDecTree dt) t
    An.Match m dt _ tb -> Match (desugarExpr m) (desugarDecTree dt) tb
    An.FunMatch dt pt bt ->
        let x = "#x"
        in Fun (x, pt) (Match (Var (TypedVar x pt)) (desugarDecTree dt) bt, bt)

M src/Infer.hs => src/Infer.hs +42 -52
@@ 23,10 23,14 @@ import NonEmpty
import qualified Ast
import Ast (Id(..), IdCase(..), idstr, scmBody, isFunLike)
import TypeErr
import AnnotAst hiding (Id)
import Match
import qualified AnnotAst
import AnnotAst hiding (Expr, Expr', Defs, Id)


type Expr' = AnnotAst.Expr' Cases
type Expr = AnnotAst.Expr Cases
type Defs = AnnotAst.Defs Cases

newtype ExpectedType = Expected Type
data FoundType = Found SrcPos Type



@@ 37,7 41,6 @@ data Env = Env
    --   types of its parameters, and the span (number of constructors) of the
    --   datatype
    , _envCtors :: Map String (VariantIx, (String, [TVar]), [Type], Span)
    , _envTypeDefs :: Map String ([TVar], [(String, [Type])])
    }
makeLenses ''Env



@@ 52,16 55,15 @@ type Infer a = ReaderT Env (StateT St (Except TypeErr)) a


inferTopDefs
    :: TypeDefs
    -> Ctors
    :: Ctors
    -> [Ast.Extern]
    -> [Ast.Def]
    -> Except TypeErr (Externs, Defs, Subst)
inferTopDefs tdefs ctors externs defs = evalStateT
inferTopDefs ctors externs defs = evalStateT
    (runReaderT inferTopDefs' initEnv)
    initSt
  where
    inferTopDefs' = augment envTypeDefs tdefs $ augment envCtors ctors $ do
    inferTopDefs' = augment envCtors ctors $ do
        externs' <- checkExterns externs
        let externs'' = fmap (Forall Set.empty) externs'
        defs' <- checkStartType defs


@@ 83,11 85,7 @@ inferTopDefs tdefs ctors externs defs = evalStateT
    checkStartDefined ds =
        when (not (Map.member "start" ds)) (throwError StartNotDefined)
    startScheme = Forall Set.empty startType
    initEnv = Env
        { _envDefs = Map.empty
        , _envCtors = Map.empty
        , _envTypeDefs = Map.empty
        }
    initEnv = Env { _envDefs = Map.empty, _envCtors = Map.empty }
    initSt = St { _tvCount = 0, _substs = Map.empty }

-- TODO: Check that the types of the externs are valid more than just not


@@ 174,7 172,7 @@ infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
        unify (Expected (TPrim TBool)) (Found (getPos p) tp)
        unify (Expected tc) (Found (getPos a) ta)
        pure (tc, If p' c' a')
    Ast.Fun p b -> inferFunMatch pos (pure (p, b))
    Ast.Fun p b -> inferFunMatch (pure (p, b))
    Ast.Let defs b -> do
        annotDefs <- inferDefs (fromList1 defs)
        let defsScms = fmap (\(scm, _) -> scm) annotDefs


@@ 187,9 185,8 @@ infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
    Ast.Match matchee cases -> do
        (tmatchee, matchee') <- infer matchee
        (tbody, cases') <- inferCases (Expected tmatchee) cases
        dt <- toDecisionTree' pos tmatchee cases'
        pure (tbody, Match matchee' dt tbody)
    Ast.FunMatch cases -> inferFunMatch pos cases
        pure (tbody, Match matchee' cases' tmatchee tbody)
    Ast.FunMatch cases -> inferFunMatch cases
    Ast.Ctor c -> inferExprConstructor c
    Ast.Box x -> fmap (\(tx, x') -> (TBox tx, Box x')) (infer x)
    Ast.Deref x -> do


@@ 198,62 195,55 @@ infer (WithPos pos e) = fmap (second (WithPos pos)) $ case e of
        unify (Expected (TBox t)) (Found (getPos x) tx)
        pure (t, Deref x')

toDecisionTree' :: SrcPos -> Type -> [(SrcPos, Pat, Expr)] -> Infer DecisionTree
toDecisionTree' pos tpat cases = do
    -- TODO: Could we do this differently, more efficiently?
    --
    -- Match needs to be able to match on the pattern types to generate proper
    -- error messages for inexhaustive patterns, so apply substitutions.
    s <- use substs
    let tpat' = subst s tpat
    let cases' = map (\(cpos, p, e) -> (cpos, substPat s p, e)) cases
    mTypeDefs <- views envTypeDefs (fmap (map fst . snd))
    lift (lift (toDecisionTree mTypeDefs pos tpat' cases'))

inferFunMatch :: SrcPos -> NonEmpty (Ast.Pat, Ast.Expr) -> Infer (Type, Expr')
inferFunMatch pos cases = do
inferFunMatch :: NonEmpty (Ast.Pat, Ast.Expr) -> Infer (Type, Expr')
inferFunMatch cases = do
    tpat <- fresh
    (tbody, cases') <- inferCases (Expected tpat) cases
    dt <- toDecisionTree' pos tpat cases'
    pure (TFun tpat tbody, FunMatch dt tpat tbody)
    pure (TFun tpat tbody, FunMatch cases' tpat tbody)

-- | All the patterns must be of the same types, and all the bodies must be of
--   the same type.
inferCases
    :: ExpectedType -- Type of matchee. Expected type of pattern.
    -> NonEmpty (Ast.Pat, Ast.Expr)
    -> Infer (Type, [(SrcPos, Pat, Expr)])
    -> Infer (Type, Cases)
inferCases tmatchee cases = do
    (tpats, tbodies, cases') <- fmap unzip3 (mapM inferCase (fromList1 cases))
    forM_ tpats (unify tmatchee)
    tbody <- fresh
    forM_ tbodies (unify (Expected tbody))
    pure (tbody, cases')
    pure (tbody, Cases cases')

inferCase
    :: (Ast.Pat, Ast.Expr) -> Infer (FoundType, FoundType, (SrcPos, Pat, Expr))
inferCase :: (Ast.Pat, Ast.Expr) -> Infer (FoundType, FoundType, (Pat, Expr))
inferCase (p, b) = do
    (tp, p', pvs) <- inferPat p
    let pvs' = Map.mapKeys Ast.idstr pvs
    (tb, b') <- withLocals' pvs' (infer b)
    let ppos = getPos p
    pure (Found ppos tp, Found (getPos b) tb, (ppos, p', b'))
    pure (Found (getPos p) tp, Found (getPos b) tb, (p', b'))

inferPat :: Ast.Pat -> Infer (Type, Pat, Map (Id 'Small) Scheme)
inferPat = \case
    Ast.PConstruction pos c ps -> inferPatConstruction pos c ps
    Ast.PInt _ n -> pure (TPrim TInt, intToPCon n 64, Map.empty)
    Ast.PBool _ b -> pure (TPrim TBool, intToPCon (fromEnum b) 1, Map.empty)
    Ast.PVar (Id (WithPos _ "_")) -> do
        tv <- fresh
        pure (tv, PWild, Map.empty)
    Ast.PVar x@(Id x') -> do
        tv <- fresh
        pure (tv, PVar (TypedVar x' tv), Map.singleton x (Forall Set.empty tv))
    Ast.PBox _ p -> do
        (tp', p', vs) <- inferPat p
        pure (TBox tp', PBox p', vs)
inferPat pat = fmap
    (\(t, p, ss) -> (t, WithPos (getPos pat) p, ss))
    (inferPat' pat)
  where
    inferPat' = \case
        Ast.PConstruction pos c ps -> inferPatConstruction pos c ps
        Ast.PInt _ n -> pure (TPrim TInt, intToPCon n 64, Map.empty)
        Ast.PBool _ b ->
            pure (TPrim TBool, intToPCon (fromEnum b) 1, Map.empty)
        Ast.PVar (Id (WithPos _ "_")) -> do
            tv <- fresh
            pure (tv, PWild, Map.empty)
        Ast.PVar x@(Id x') -> do
            tv <- fresh
            pure
                ( tv
                , PVar (TypedVar x' tv)
                , Map.singleton x (Forall Set.empty tv)
                )
        Ast.PBox _ p -> do
            (tp', p', vs) <- inferPat p
            pure (TBox tp', PBox p', vs)
    intToPCon n w = PCon
        (Con
            { variant = fromIntegral n


@@ 267,7 257,7 @@ inferPatConstruction
    :: SrcPos
    -> Id 'Big
    -> [Ast.Pat]
    -> Infer (Type, Pat, Map (Id 'Small) Scheme)
    -> Infer (Type, Pat', Map (Id 'Small) Scheme)
inferPatConstruction pos c cArgs = do
    (variantIx, tdefLhs, cParams, cSpan) <- lookupEnvConstructor c
    let arity = length cParams

M src/Match.hs => src/Match.hs +14 -25
@@ 4,7 4,7 @@
--   and partial evaluation/ by Peter Sestoft. Close to 1:1, and includes the
--   additional checks for exhaustiveness and redundancy described in section
--   7.4.
module Match (toDecisionTree, Span, Con(..), Pat(..), MTypeDefs) where
module Match (toDecisionTree, Span, Con(..), MTypeDefs) where

import Prelude hiding (span)
import qualified Data.Set as Set


@@ 23,22 23,11 @@ import Control.Lens (makeLenses, view, views)
import Misc hiding (augment)
import SrcPos
import TypeErr
import AnnotAst
import qualified AnnotAst
import AnnotAst hiding (Expr)


data Con = Con
    { variant :: VariantIx
    , span :: Span
    , argTs :: [Type]
    }
    deriving Show

data Pat
    = PVar TypedVar
    | PWild
    | PCon Con [Pat]
    | PBox Pat
    deriving Show
type Expr = AnnotAst.Expr DecisionTree

data Descr = Pos Con [Descr] | Neg (Set Con)
    deriving Show


@@ 77,12 66,12 @@ toDecisionTree
    :: MTypeDefs
    -> SrcPos
    -> Type
    -> [(SrcPos, Pat, Expr)]
    -> [(Pat, Expr)]
    -> Except TypeErr DecisionTree
toDecisionTree tds ePos tp cases =
    let
        rules = map (\(pos, p, e) -> (p, (pos, Map.empty, e))) cases
        redundantCases = map (\(pos, _, _) -> pos) cases
        rules = map (\(WithPos pos p, e) -> (p, (pos, Map.empty, e))) cases
        redundantCases = map (getPos . fst) cases
    in do
        let env = Env { _tdefs = tds, _tpat = tp, _exprPos = ePos }
        (d, redundantCases') <- runStateT


@@ 91,10 80,10 @@ toDecisionTree tds ePos tp cases =
        forM_ redundantCases' $ throwError . RedundantCase
        pure (switchify d)

compile :: [(Pat, Rhs)] -> Match DecisionTree'
compile :: [(Pat', Rhs)] -> Match DecisionTree'
compile = disjunct (Neg Set.empty)

disjunct :: Descr -> [(Pat, Rhs)] -> Match DecisionTree'
disjunct :: Descr -> [(Pat', Rhs)] -> Match DecisionTree'
disjunct descr = \case
    [] -> do
        patStr <- view tpat >>= flip missingPat descr


@@ 137,13 126,13 @@ match
    -> Ctx
    -> Work
    -> Rhs
    -> [(Pat, Rhs)]
    -> Pat
    -> [(Pat', Rhs)]
    -> Pat'
    -> Match DecisionTree'
match obj descr ctx work rhs rules = \case
    PVar x -> conjunct (augment descr ctx) (addBind x obj rhs) rules work
    PWild -> conjunct (augment descr ctx) rhs rules work
    PBox p -> match (ADeref obj) descr ctx work rhs rules p
    PBox (WithPos _ p) -> match (ADeref obj) descr ctx work rhs rules p
    PCon pcon pargs ->
        let
            disjunct' :: Descr -> Match DecisionTree'


@@ 175,12 164,12 @@ match obj descr ctx work rhs rules = \case
                no <- disjunct' (addneg pcon descr)
                pure (IfEq obj pcon yes no)

conjunct :: Ctx -> Rhs -> [(Pat, Rhs)] -> Work -> Match DecisionTree'
conjunct :: Ctx -> Rhs -> [(Pat', Rhs)] -> Work -> Match DecisionTree'
conjunct ctx rhs@(casePos, binds, e) rules = \case
    [] -> caseReached casePos $> Success (binds, e)
    (work1 : workr) -> case work1 of
        ([], [], []) -> conjunct (norm ctx) rhs rules workr
        (pat1 : patr, obj1 : objr, descr1 : descrr) ->
        (WithPos _ pat1 : patr, obj1 : objr, descr1 : descrr) ->
            match obj1 descr1 ctx ((patr, objr, descrr) : workr) rhs rules pat1
        x -> ice $ "unexpected pattern in conjunct: " ++ show x


M src/Misc.hs => src/Misc.hs +6 -0
@@ 12,6 12,7 @@ module Misc
    , showChar''
    , showChar'
    , both
    , secondM
    , augment
    , insertWith'
    , if'


@@ 25,6 26,7 @@ import Data.Map (Map)
import Data.Composition
import Control.Monad.Reader
import Control.Lens (Lens', locally)
import Data.Bitraversable
import System.Exit
import LLVM.AST.Type (Type)
import LLVM.AST (Name, Module)


@@ 92,6 94,10 @@ showChar' c = "'" ++ showChar'' c ++ "'"
both :: (a -> b) -> (a, a) -> (b, b)
both f (a0, a1) = (f a0, f a1)

secondM
    :: (Bitraversable t, Applicative f) => (b -> f b') -> t a b -> f (t a b')
secondM = bimapM pure

augment
    :: (MonadReader e m, Ord k) => Lens' e (Map k v) -> Map k v -> m a -> m a
augment l = locally l . Map.union

M src/Subst.hs => src/Subst.hs +12 -25
@@ 7,8 7,12 @@ import Data.Map.Strict (Map)
import Data.Bifunctor
import Data.Maybe

import Match
import AnnotAst
import qualified AnnotAst as An
import AnnotAst hiding (Defs, Expr)


type Defs = An.Defs Cases
type Expr = An.Expr Cases

-- | Map of substitutions from type-variables to more specific types
type Subst = Map TVar Type


@@ 26,36 30,19 @@ substExpr s (WithPos p e) = WithPos p $ case e of
    App f a rt -> App (substExpr s f) (substExpr s a) (subst s rt)
    If p c a -> If (substExpr s p) (substExpr s c) (substExpr s a)
    Let defs body -> Let (fmap (substDef s) defs) (substExpr s body)
    Match e dt tbody ->
        Match (substExpr s e) (substDecisionTree s dt) (subst s tbody)
    FunMatch dt tp tb ->
        FunMatch (substDecisionTree s dt) (subst s tp) (subst s tb)
    Match e cs tp tbody ->
        Match (substExpr s e) (substCases s cs) (subst s tp) (subst s tbody)
    FunMatch cs tp tb -> FunMatch (substCases s cs) (subst s tp) (subst s tb)
    Ctor i span' (tx, tts) ps ->
        Ctor i span' (tx, map (subst s) tts) (map (subst s) ps)
    Box e -> Box (substExpr s e)
    Deref e -> Deref (substExpr s e)

substDecisionTree :: Subst -> DecisionTree -> DecisionTree
substDecisionTree s = \case
    DSwitch obj cs def -> DSwitch
        (substAccess s obj)
        (fmap (substDecisionTree s) cs)
        (substDecisionTree s def)
    DLeaf (bs, e) -> DLeaf
        ( Map.fromList
            (map (bimap (substTypedVar s) (substAccess s)) (Map.toList bs))
        , substExpr s e
        )

substAccess :: Subst -> Access -> Access
substAccess s = \case
    Obj -> Obj
    As a span' ts -> As (substAccess s a) span' (map (subst s) ts)
    Sel i span' a -> Sel i span' (substAccess s a)
    ADeref a -> ADeref (substAccess s a)
substCases :: Subst -> Cases -> Cases
substCases s (Cases cs) = Cases (map (bimap (substPat s) (substExpr s)) cs)

substPat :: Subst -> Pat -> Pat
substPat s = \case
substPat s (WithPos pos pat) = WithPos pos $ case pat of
    PWild -> PWild
    PVar v -> PVar (substTypedVar s v)
    PBox p -> PBox (substPat s p)