cleanup: Delete unused VSum (#76)

brat/Brat/Checker/SolveHoles.hs

@@ -11,7 +11,6 @@ import Brat.Syntax.Value
 import Control.Monad.Freer
 import Bwd
 import Hasochism
-import Util (zipSameLength)
 
 import Control.Monad (when)
 import Data.Bifunctor (second)
@@ -161,10 +160,4 @@ typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> ou
   probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg
         (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd
   sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
-typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1)
-  | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of
-      Nothing -> typeErr "Mismatched sum lengths"
-      Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat)
- where
-  eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1)
 typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1)

brat/Brat/Compile/Hugr.hs

@@ -164,9 +164,6 @@ compileType ty@(TCons _ _) = htTuple (tuple ty)
   tuple TNil = []
   tuple ty = error $ "Found " ++ show ty  ++ " in supposed tuple type"
 compileType TNil = htTuple []
-compileType (VSum my ros) = case my of
-  Braty -> error "Todo: compileTypeWorker for BRAT"
-  Kerny -> HTSum (SG (GeneralSum $ map (\(Some ro) -> compileRo ro) ros))
 compileType (TVec el _) = hugrList (compileType el)
 compileType (TList el)  = hugrList (compileType el)
 -- All variables are of kind `TypeFor m xs`, we already checked in `kindCheckRow`

brat/Brat/Eval.hs

@@ -88,7 +88,6 @@ sem ga (VApp f vz) = do
     f <- semVar ga f
     vz <- traverse (sem ga) vz
     applySem f vz
-sem ga (VSum my ts) = pure $ SSum my ga ts
 
 semVar :: Stack Z Sem n -> VVar n -> Checking Sem
 semVar vz (VInx inx) = pure $ proj vz inx
@@ -125,10 +124,6 @@ quote lvy (SLam stk body) = do
   VLam <$> quote (Sy lvy) body
 quote lvy (SFun my ga cty) = VFun my <$> quoteCTy lvy my ga cty
 quote lvy (SApp f vz) = VApp (quoteVar lvy f) <$> traverse (quote lvy) vz
-quote lvy (SSum my ga ts) = VSum my <$> traverse quoteVariant ts
-  where
-  quoteVariant (Some ro) = quoteRo my ga ro lvy >>= \case
-    (_, Some (ro :* _)) -> pure (Some ro)
 
 quoteCTy :: Ny lv -> Modey m -> Stack Z Sem n -> CTy m n -> Checking (CTy m lv)
 quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case
@@ -320,7 +315,6 @@ doesntOccur e (VLam body) = doesntOccur e body
 doesntOccur e (VFun my (ins :->> outs)) = case my of
   Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
   Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
-doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows
 
 collision :: End -> End -> Either ErrorMsg ()
 collision e v | e == v = Left . UnificationError $

brat/Brat/Syntax/Value.hs

@@ -157,7 +157,6 @@ data Val :: N -> Type where
   VLam :: Val (S n) -> Val n -- Just body (binds DeBruijn index n)
   VFun :: MODEY m => Modey m -> CTy m n -> Val n
   VApp :: VVar n -> Bwd (Val n) -> Val n
-  VSum :: MODEY m => Modey m -> [Some (Ro m n)] -> Val n -- (Hugr-like) Sum types
 
 data SVar = SPar End | SLvl Int
  deriving (Show, Eq)
@@ -223,12 +222,6 @@ instance Show (Val n) where
   show (VFun m cty) = "{ " ++ modily m (show cty) ++ " }"
   show (VApp v ctx) = "VApp " ++ show v ++ " " ++ show ctx
   show (VLam body) = "VLam " ++ show body
-  show (VSum my ros) = case my of
-    Braty -> "VSum (" ++ intercalate " + " (helper <$> ros) ++ ")"
-    Kerny -> "VSum (" ++ intercalate " + " (helper <$> ros) ++ ")"
-   where
-    helper :: MODEY m => Some (Ro m n) -> String
-    helper (Some ro) = show ro
 
 ---------------------------------- Patterns -----------------------------------
 pattern TNat, TInt, TFloat, TBool, TText, TUnit, TNil :: Val n
@@ -524,9 +517,6 @@ instance DeBruijn Val where
     = VFun Braty $ changeVar vc cty
   changeVar vc (VFun Kerny cty)
     = VFun Kerny $ changeVar vc cty
-  changeVar vc (VSum my ros)
-    = VSum my (f <$> ros)
-    where f (Some ro) = case varChangerThroughRo vc ro of Some (_ :* ro) -> Some ro
 
 varChangerThroughRo :: VarChanger src tgt
                     -> Ro m src src'