adding and pruning ctors

Ctors.hs

{-# LANGUAGE DataKinds, TypeApplications #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Main where

import Data.RBR (FromList,Insert,Delete,Variant,I,injectSubset,widen,injectI,winnowI,prettyShowVariantI)

import GHC.TypeLits

-- would defining these as nullary type families improve things?
type Phase01 = FromList '[ '("ctor1",Int), '("ctor2",Bool), '("ctor3",Char) ]

type Phase02 = Insert "ctor4" Int Phase01

type Phase03 = Delete "ctor1" Int Phase02

-- easy to move between these phases because the set of constructors becomes bigger
fromPhase1ToPhase2 :: Variant I Phase01 -> Variant I Phase02
fromPhase1ToPhase2 = injectSubset --  widen @"ctor4" would also work here, and with less work for the compiler

-- we have to winnow the "ctor1" constructor that is absent in the new phase. We convert it into a ctor2
fromPhase2ToPhase3 :: Variant I Phase02 -> Variant I Phase03
fromPhase2ToPhase3 v = case winnowI @"ctor1" @Int v of 
    Right z -> injectI @"ctor2" False
    Left v' -> injectSubset v' -- here the injectSubset is not strictly needed but in more complex cases, it could be.
                               -- removing it will likely improve compilation times.

main :: IO ()
main = print (prettyShowVariantI (fromPhase2ToPhase3 (fromPhase1ToPhase2 (injectI @"ctor1" 2))))