Syntax.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE PatternSynonyms #-}

-- The raw abstract syntax and (refined) abstract syntax for Frank
module Syntax where

import qualified Data.Map.Strict as M
import Data.List

{-------------------}
{-- For the definition of the AST --}

data Fix f = Fx (f (Fix f))
deriving instance Show (f (Fix f)) => Show (Fix f)
deriving instance Eq (f (Fix f)) => Eq (Fix f)

data AnnotT a f r = AnnF (f r, a)
deriving instance (Show (f r), Show a) => Show (AnnotT a f r)
deriving instance (Eq (f r), Eq a) => Eq (AnnotT a f r)

type AnnotFix f a = Fix (AnnotT a (f a))

ann :: a -> f a (AnnotFix f a) -> AnnotFix f a
ann a v = (Fx (AnnF (v, a)))

unAnn :: AnnotFix f a -> (f a (AnnotFix f a), a)
unAnn (Fx (AnnF (v, a))) = (v, a)

strip :: AnnotFix f a -> f a (AnnotFix f a)
strip = fst . unAnn

attr :: AnnotFix f a -> a
attr = snd . unAnn

splitAnn :: Fix (AnnotT a f) -> (Fix (AnnotT a f), f (Fix (AnnotT a f)), a)
splitAnn x@(Fx (AnnF (v, a))) = (x , v, a)

liftAnn :: (Monad m) => (f a (AnnotFix f a) -> m (f a (AnnotFix f a))) -> AnnotFix f a -> m (AnnotFix f a)
liftAnn f (unAnn -> (v, a)) = ann a <$> f v

keepAnn :: (f a (AnnotFix f a) -> f a (AnnotFix f a)) -> AnnotFix f a -> AnnotFix f a
keepAnn f (unAnn -> (v, a)) = ann a (f v)

data Source = InCode (Integer, Integer)
            | BuiltIn
            | Implicit
            | ImplicitNear (Integer, Integer)
            | Generated
  deriving (Show, Eq)

class HasSource a where
  getSource :: a -> Source
instance HasSource a => HasSource (AnnotFix f a) where
  getSource x = getSource (attr x)

implicitNear :: HasSource a => a -> Source
implicitNear v = case getSource v of InCode (line, col) -> ImplicitNear (line, col)
                                     _                  -> Implicit

{-------------------}
{-- Syntax description: raw syntax comes from the parser and preprocessed into
    refined syntax. --}

class NotRaw a where
  idNotRaw :: a -> a

class NotDesugared a where
  idNotDesugared :: a -> a

-- output from the parser
newtype Raw = Raw Source
  deriving (Show, Eq)
instance NotDesugared Raw where idNotDesugared = Prelude.id
instance HasSource Raw where getSource (Raw s) = s

instance NotRaw () where idNotRaw = Prelude.id

-- well-formed AST (after tidying up the output from the parser)
newtype Refined = Refined Source
  deriving (Show, Eq)
instance NotDesugared Refined where idNotDesugared = Prelude.id
instance NotRaw Refined where idNotRaw = Prelude.id
instance HasSource Refined where getSource (Refined s) = s

-- desugaring of types:
--   * type variables are given unique names
--   * strings are lists of characters
newtype Desugared = Desugared Source
  deriving (Show, Eq)
instance NotRaw Desugared where idNotRaw = Prelude.id
instance HasSource Desugared where getSource (Desugared s) = s

{-- The raw syntax as parsed in from the file and the refined syntax produced
    by a preprocessing stage before typechecking are simultaneously defined
    using GADT syntax. --}

data Prog t = MkProg [TopTm t]
deriving instance Show t => Show (Prog t)
deriving instance Eq t => Eq (Prog t)

{---------------}
{- Parts of the grammar specific to the raw syntax. -}

-- A top-level multihandler signature and clause.
-- data MHSigF r = MkSig Id (CType Raw) deriving (Show, Eq)
-- type MHSig = Fix (AnnotT Source MHSigF)
data MHSigF :: * -> * -> * where
  MkSig :: Id -> CType Raw -> MHSigF Raw r
deriving instance Show (MHSigF Raw r)
deriving instance Eq (MHSigF Raw r)
type MHSig t = AnnotFix MHSigF t
pattern Sig x cty a = Fx (AnnF (MkSig x cty, a))

data MHClsF :: * -> * -> * where
  MkMHCls :: Id -> Clause Raw -> MHClsF Raw r
deriving instance Show (MHClsF t r)
deriving instance Eq (MHClsF t r)
type MHCls t = AnnotFix MHClsF t
pattern MHCls x cls a = Fx (AnnF (MkMHCls x cls, a))

{---------------}
{- Parts of the grammar specific to the refined syntax. -}

-- FIXME: currently all top-level bindings are mutually
-- recursive. This setup will break if we add non-recursive value
-- bindings.
--
-- An obvious design is to group mutually recursive bindings using
-- letrec, as specified in the paper.
--
-- Data and interface definitions can continue to be globally mutually
-- recursive as they do not depend on values.

-- a recursive multihandler definition
data MHDefF :: * -> * -> * where
  MkDef :: Id -> CType t -> [Clause t] -> MHDefF t r
deriving instance Show t => Show (MHDefF t r)
deriving instance Eq t => Eq (MHDefF t r)
type MHDef t = AnnotFix MHDefF t
pattern Def x cty clss a = Fx (AnnF (MkDef x cty clss, a))
-- value bindings - not yet supported
-- data VDef a = VDef Id (VType a) (Tm a)

{- MH here = 'operator' in the paper. Operator here doesn't have a name
   in the paper. -}

data OperatorF :: * -> * -> * where
  MkMono :: Id -> OperatorF t r  -- monotypic (just variable)
  MkPoly :: Id -> OperatorF t r  -- polytypic  (handler expecting arguments, could also be 0 args (!))
  MkCmdId :: Id -> OperatorF t r
deriving instance Show t => Show (OperatorF t r)
deriving instance Eq t => Eq (OperatorF t r)
type Operator t = AnnotFix OperatorF t
pattern Mono x a = Fx (AnnF (MkMono x, a))
pattern Poly x a = Fx (AnnF (MkPoly x, a))
pattern CmdId x a = Fx (AnnF (MkCmdId x, a))

data DataConF :: * -> * -> * where
  MkDataCon :: Id -> [Tm t] -> DataConF t r
deriving instance Show t => Show (DataConF t r)
deriving instance Eq t => Eq (DataConF t r)
type DataCon t = AnnotFix DataConF t
pattern DataCon x tms a = Fx (AnnF (MkDataCon x tms, a))

{---------------}
{- Parts of the grammar independent of the syntax. -}

-- A raw term collects multihandler signatures and clauses separately. A
-- refined top-level term collects multihandler signatures and clauses in one
-- definition.
data TopTmF :: * -> * -> * where
  MkDataTm :: DataT t -> TopTmF t r
  MkItfTm :: Itf t -> TopTmF t r
  MkItfAliasTm :: ItfAlias t -> TopTmF t r
  MkSigTm :: MHSig Raw -> TopTmF Raw r
  MkClsTm :: MHCls Raw -> TopTmF Raw r
  MkDefTm :: NotRaw t => MHDef t -> TopTmF t r
deriving instance Show t => Show (TopTmF t r)
deriving instance Eq t => Eq (TopTmF t r)
type TopTm t = AnnotFix TopTmF t
pattern DataTm dt a = Fx (AnnF (MkDataTm dt, a))
pattern ItfTm itf a = Fx (AnnF (MkItfTm itf, a))
pattern ItfAliasTm itfAl a = Fx (AnnF (MkItfAliasTm itfAl, a))
pattern SigTm sig a = Fx (AnnF (MkSigTm sig, a))
pattern ClsTm cls a = Fx (AnnF (MkClsTm cls, a))
pattern DefTm def a = Fx (AnnF (MkDefTm def, a))

data UseF :: * -> * -> * where
  MkRawId :: Id -> UseF Raw r
  MkRawComb :: r -> [Tm Raw] -> UseF Raw r
  MkOp :: NotRaw t => Operator t -> UseF t r
  MkApp :: NotRaw t => r -> [Tm t] -> UseF t r
deriving instance (Show r, Show (Tm t), Show t) => Show (UseF t r)
deriving instance (Eq r, Eq (Tm t), Eq t) => Eq (UseF t r)
type Use t = AnnotFix UseF t
pattern RawId x a = Fx (AnnF (MkRawId x, a))
pattern RawComb f xs a = Fx (AnnF (MkRawComb f xs, a))
pattern Op op a = Fx (AnnF (MkOp op, a))
pattern App f xs a = Fx (AnnF (MkApp f xs, a))

-- Tm here = 'construction' in the paper

data TmF :: * -> * -> * where
  MkSC :: SComp t -> TmF t r
  MkLet :: Id -> r -> r -> TmF Raw r
  MkStr :: String -> TmF t r
  MkInt :: Integer -> TmF t r
  MkChar :: Char -> TmF t r
  MkList :: [r] -> TmF Raw r
  MkTmSeq :: r -> r -> TmF t r
  MkUse :: Use t -> TmF t r
  MkDCon :: NotRaw t => DataCon t -> TmF t r
deriving instance (Show r, Show t) => Show (TmF t r)
deriving instance (Eq r, Eq t) => Eq (TmF t r)
type Tm t = AnnotFix TmF t
pattern SC sc a = Fx (AnnF (MkSC sc, a))
pattern Let x tm1 tm2 a = Fx (AnnF (MkLet x tm1 tm2, a))
pattern StrTm str a = Fx (AnnF (MkStr str, a))
pattern IntTm n a = Fx (AnnF (MkInt n, a))
pattern CharTm c a = Fx (AnnF (MkChar c, a))
pattern ListTm xs a = Fx (AnnF (MkList xs, a))
pattern TmSeq tm1 tm2 a = Fx (AnnF (MkTmSeq tm1 tm2, a))
pattern Use u a = Fx (AnnF (MkUse u, a))
pattern DCon dc a = Fx (AnnF (MkDCon dc, a))

-- A clause for a multihandler definition
data ClauseF :: * -> * -> * where
  MkCls :: [Pattern t] -> Tm t -> ClauseF t r
deriving instance Show t => Show (ClauseF t r)
deriving instance Eq t => Eq (ClauseF t r)
type Clause t = AnnotFix ClauseF t
pattern Cls ps t a = Fx (AnnF (MkCls ps t, a))

data SCompF :: * -> * -> * where
  MkSComp :: [Clause t] -> SCompF t r
deriving instance Show t => Show (SCompF t r)
deriving instance Eq t => Eq (SCompF t r)
type SComp t = AnnotFix SCompF t
pattern SComp cls a = Fx (AnnF (MkSComp cls, a))

data Kind = VT   -- value type
          | ET   -- effect type
  deriving (Show, Eq)

data DataTF :: * -> * -> * where
  MkDT :: Id -> [(Id, Kind)] -> [Ctr t] -> DataTF t r
deriving instance Show t => Show (DataTF t r)
deriving instance Eq t => Eq (DataTF t r)
type DataT t = AnnotFix DataTF t
pattern DT x ps ctrs a = Fx (AnnF ((MkDT x ps ctrs), a))

data ItfF :: * -> * -> * where
  MkItf :: Id -> [(Id, Kind)] -> [Cmd t] -> ItfF t r
deriving instance Show t => Show (ItfF t r)
deriving instance Eq t => Eq (ItfF t r)
type Itf t = AnnotFix ItfF t
pattern Itf x ps cmds a = Fx (AnnF (MkItf x ps cmds, a))

data ItfAliasF :: * -> * -> * where
  MkItfAlias :: Id -> [(Id, Kind)] -> (ItfMap t) -> ItfAliasF t r
deriving instance Show t => Show (ItfAliasF t r)
deriving instance Eq t => Eq (ItfAliasF t r)
type ItfAlias t = AnnotFix ItfAliasF t
pattern ItfAlias x ps itfMap a = Fx (AnnF (MkItfAlias x ps itfMap, a))

data CtrF :: * -> * -> * where
  MkCtr :: Id -> [VType t] -> CtrF t r
deriving instance Show t => Show (CtrF t r)
deriving instance Eq t => Eq (CtrF t r)
type Ctr t = AnnotFix CtrF t
pattern Ctr x tys a = Fx (AnnF (MkCtr x tys, a))

data CmdF :: * -> * -> * where
  MkCmd :: Id -> [(Id, Kind)] -> [VType t] -> VType t -> CmdF t r
deriving instance Show t => Show (CmdF t r)
deriving instance Eq t => Eq (CmdF t r)
--                    id  ty vars      arg tys   result ty
type Cmd t = AnnotFix CmdF t
pattern Cmd x ps tys ty a = Fx (AnnF (MkCmd x ps tys ty, a))

data PatternF :: * -> * -> * where
  MkVPat :: ValuePat t -> PatternF t r
  MkCmdPat :: Id -> [ValuePat t] -> Id -> PatternF t r
  MkThkPat :: Id -> PatternF t r
deriving instance Show t => Show (PatternF t r)
deriving instance Eq t => Eq (PatternF t r)
type Pattern t = AnnotFix PatternF t
pattern VPat vp a = Fx (AnnF (MkVPat vp, a))
pattern CmdPat x vps k a = Fx (AnnF (MkCmdPat x vps k, a))
pattern ThkPat x a = Fx (AnnF (MkThkPat x, a))

-- TODO: should we compile away string patterns into list of char patterns?
data ValuePatF :: * -> * -> * where
  MkVarPat :: Id -> ValuePatF t r
  MkDataPat :: Id -> [r] -> ValuePatF t r
  MkIntPat :: Integer -> ValuePatF t r
  MkCharPat :: Char -> ValuePatF t r
  MkStrPat :: String -> ValuePatF t r
  MkConsPat :: r -> r -> ValuePatF Raw r
  MkListPat :: [r] -> ValuePatF Raw r
deriving instance (Show r, Show t) => Show (ValuePatF t r)
deriving instance (Eq r, Eq t) => Eq (ValuePatF t r)
type ValuePat t = AnnotFix ValuePatF t
pattern VarPat x a = Fx (AnnF (MkVarPat x, a))
pattern DataPat x vps a = Fx (AnnF (MkDataPat x vps, a))
pattern IntPat n a = Fx (AnnF (MkIntPat n, a))
pattern CharPat c a = Fx (AnnF (MkCharPat c, a))
pattern StrPat str a = Fx (AnnF (MkStrPat str, a))
pattern ConsPat p1 p2 a = Fx (AnnF (MkConsPat p1 p2, a))
pattern ListPat ps a = Fx (AnnF (MkListPat ps, a))

type Id = String

-- Type hierarchy
data CTypeF :: * -> * -> * where
  MkCType :: [Port t] -> Peg t -> CTypeF t r     -- computation types
deriving instance Show t => Show (CTypeF t r)
deriving instance Eq t => Eq (CTypeF t r)
type CType t= AnnotFix CTypeF t
pattern CType ports peg a = Fx (AnnF (MkCType ports peg, a))

data PortF :: * -> * -> * where
  MkPort :: Adj t -> VType t -> PortF t r       -- ports
deriving instance Show t => Show (PortF t r)
deriving instance Eq t => Eq (PortF t r)
type Port t = AnnotFix PortF t
pattern Port adj ty a = Fx (AnnF (MkPort adj ty, a))

data PegF :: * -> * -> * where
  MkPeg :: Ab t -> VType t -> PegF t r          -- pegs
deriving instance Show t => Show (PegF t r)
deriving instance Eq t => Eq (PegF t r)
type Peg t = AnnotFix PegF t
pattern Peg ab ty a = Fx (AnnF (MkPeg ab ty, a))

data VTypeF :: * -> * -> * where   -- value types
  MkDTTy :: Id -> [TyArg t] -> VTypeF t r       --   data types (instant. type constr.)  may be refined to MkTVar
  MkSCTy :: CType t -> VTypeF t  r              --   suspended computation types
  MkTVar :: NotDesugared t => Id -> VTypeF t  r --                                       may be refined to MkDTTy
  MkRTVar :: Id -> VTypeF Desugared r          --   rigid type variable (bound)
  MkFTVar :: Id -> VTypeF Desugared r         --   flexible type variable (free)
  MkStringTy :: NotDesugared t => VTypeF t r   --   string type
  MkIntTy :: VTypeF t r                        --   int type
  MkCharTy :: VTypeF t r                       --   char type
deriving instance Show t => Show (VTypeF t r)
deriving instance Eq t => Eq (VTypeF t r)
type VType t = AnnotFix VTypeF t
pattern DTTy x tyArgs a = Fx (AnnF (MkDTTy x tyArgs, a))
pattern SCTy cty a = Fx (AnnF (MkSCTy cty, a))
pattern TVar x a = Fx (AnnF (MkTVar x, a))
pattern RTVar x a = Fx (AnnF (MkRTVar x, a))
pattern FTVar x a = Fx (AnnF (MkFTVar x, a))
pattern StringTy a = Fx (AnnF (MkStringTy, a))
pattern IntTy a = Fx (AnnF (MkIntTy, a))
pattern CharTy a = Fx (AnnF (MkCharTy, a))

data ItfMapF :: * -> * -> * where
  MkItfMap :: M.Map Id [TyArg t] -> ItfMapF t r           -- interface-id  ->  list of ty arg's  (each entry an instantiation)
deriving instance Show t => Show (ItfMapF t r)
deriving instance Eq t => Eq (ItfMapF t r)
type ItfMap t = AnnotFix ItfMapF t
pattern ItfMap m a = Fx (AnnF (MkItfMap m, a))

-- Adjustments (set of instantiated interfaces)
data AdjF :: * -> * -> * where
  MkAdj :: ItfMap t -> AdjF t r                -- interface-id  ->  list of ty arg's
deriving instance Show t => Show (AdjF t r)
deriving instance Eq t => Eq (AdjF t r)
type Adj t = AnnotFix AdjF t
pattern Adj itfMap a = Fx (AnnF (MkAdj itfMap, a))

-- Abilities
data AbF :: * -> * -> * where
  MkAb :: AbMod t -> ItfMap t -> AbF t r        -- interface-id  ->  list of ty arg's
deriving instance Show t => Show (AbF t r)
deriving instance Eq t => Eq (AbF t r)
type Ab t = AnnotFix AbF t
pattern Ab abMod itfMap a = Fx (AnnF (MkAb abMod itfMap, a))

-- Ability modes
data AbModF :: * -> * -> * where
  MkEmpAb :: AbModF t r                         -- empty            (closed ability)
  MkAbVar :: NotDesugared t => Id -> AbModF t r -- non-desugared effect variable
  MkAbRVar :: Id -> AbModF Desugared r         -- rigid eff var    (open ability)
  MkAbFVar :: Id -> AbModF Desugared r         -- flexible eff var (open ability)
deriving instance Show (AbModF t r)
deriving instance Eq (AbModF t r)
type AbMod t = AnnotFix AbModF t
pattern EmpAb a = Fx (AnnF (MkEmpAb, a))
pattern AbVar x a = Fx (AnnF (MkAbVar x, a))
pattern AbRVar x a = Fx (AnnF (MkAbRVar x, a))
pattern AbFVar x a = Fx (AnnF (MkAbFVar x, a))

data TyArgF :: * -> * -> * where
  MkVArg :: VType t -> TyArgF t r
  MkEArg :: Ab t    -> TyArgF t r
deriving instance Show t => Show (TyArgF t r)
deriving instance Eq t => Eq (TyArgF t r)
type TyArg t = AnnotFix TyArgF t
pattern VArg ty a = Fx (AnnF (MkVArg ty, a))
pattern EArg ab a = Fx (AnnF (MkEArg ab, a))

idAdjRaw :: Adj Raw
idAdjRaw = Adj (ItfMap M.empty (Raw Implicit)) (Raw Implicit)

idAdjRef :: Adj Refined
idAdjRef = Adj (ItfMap M.empty (Refined Implicit)) (Refined Implicit)

idAdjDesug :: Adj Desugared
idAdjDesug = Adj (ItfMap M.empty (Desugared Implicit)) (Desugared Implicit)

desugaredStrTy :: Desugared -> VType Desugared
desugaredStrTy a = DTTy "List" [VArg (CharTy a) a] a

getItfs :: [TopTm t] -> [Itf t]
getItfs xs = [ itf | (ItfTm itf _) <- xs ]

getCmds :: Itf t -> [Cmd t]
getCmds (Itf _ _ xs _) = xs

getItfAliases :: [TopTm t] -> [ItfAlias t]
getItfAliases xs = [itfAlias | (ItfAliasTm itfAlias _) <- xs]

collectINames :: [Itf t] -> [Id]
collectINames = map (\case (Itf itf _ _ _) -> itf)

getDataTs :: [TopTm t] -> [DataT t]
getDataTs xs = [dt | (DataTm dt _) <- xs]

getCtrs :: DataT t -> [Ctr t]
getCtrs (DT _ _ xs _) = xs

collectDTNames :: [DataT t] -> [Id]
collectDTNames = map (\case (DT dt _ _ _) -> dt)

getDefs :: NotRaw t => [TopTm t] -> [MHDef t]
getDefs xs = [ def | (DefTm def _) <- xs ]

-- Convert ability to a list of interface names and effect variables
{-
abToList :: Ab a -> [Id]
abToList MkEmpAb = []
abToList (MkAbVar id) = [id]
abToList MkOpenAb = []
abToList (MkAbPlus ab id _) = id : abToList ab

-- Substitute the ability for the distinguished effect variable in the type.
substOpenAb :: Ab a -> VType a -> VType a
substOpenAb ab (MkDTTy id abs xs) =
  MkDTTy id (map (substOpenAbAb ab) abs) (map (substOpenAb ab) xs)
substOpenAb ab (MkSCTy cty) = MkSCTy $ substOpenAbCType ab cty
substOpenAb _ ty = ty

substOpenAbAb :: Ab a -> Ab a -> Ab a
substOpenAbAb ab MkEmpAb = MkEmpAb
substOpenAbAb ab MkOpenAb = ab
substOpenAbAb ab (MkAbVar x) = MkAbVar x
substOpenAbAb ab (MkAbPlus ab' x ts) =
  MkAbPlus (substOpenAbAb ab' ab) x (map (substOpenAb ab) ts)

substOpenAbAdj :: Ab a -> Adj a -> Adj a
substOpenAbAdj ab MkIdAdj = MkIdAdj
substOpenAbAdj ab (MkAdjPlus adj itf xs) =
  MkAdjPlus (substOpenAbAdj ab adj) itf (map (substOpenAb ab) xs)

substOpenAbCType :: Ab a -> CType a -> CType a
substOpenAbCType ab (MkCType ps q) =
  MkCType (map (substOpenAbPort ab) ps) (substOpenAbPeg ab q)

substOpenAbPeg :: Ab a -> Peg a -> Peg a
substOpenAbPeg ab (MkPeg ab' ty) =
  MkPeg (substOpenAbAb ab ab') (substOpenAb ab ty)

substOpenAbPort :: Ab a -> Port a -> Port a
substOpenAbPort ab (MkPort adj ty) =
  MkPort (substOpenAbAdj ab adj) (substOpenAb ab ty)
-}

-- ability (1st arg) might be overridden by adjustment (2nd arg)
plus :: Ab t -> Adj t -> Ab t
plus (Ab v (ItfMap m b) a) (Adj (ItfMap m' c) _) = Ab v (ItfMap (M.union m' m) b) a

getOpName :: Operator t -> Id
getOpName (Mono x _) = x
getOpName (Poly x _) = x
getOpName (CmdId x _) = x

-- transform type variable (+ its kind) to a raw tye variable argument
-- (use during refinement of itf maps)
tyVar2rawTyVarArg :: (Id, Kind) -> TyArg Raw
tyVar2rawTyVarArg (id, VT) = VArg (TVar id (Raw Generated)) (Raw Generated)
tyVar2rawTyVarArg (id, ET) = EArg (liftAbMod (AbVar id (Raw Generated))) (Raw Generated)

-- transform type variable (+ its kind) to a rigid tye variable argument
-- (prepare for later unification)
tyVar2rigTyVarArg :: (Id, Kind) -> TyArg Desugared
tyVar2rigTyVarArg (id, VT) = VArg (RTVar id (Desugared Generated)) (Desugared Generated)
tyVar2rigTyVarArg (id, ET) = EArg (liftAbMod (AbRVar id (Desugared Generated))) (Desugared Generated)

liftAbMod :: AbMod t -> Ab t
liftAbMod abMod = Ab abMod (ItfMap M.empty (attr abMod)) (attr abMod)

-- Only to be applied to identifiers representing rigid or flexible
-- metavariables (type or effect).
trimVar :: Id -> Id
trimVar = takeWhile (/= '$')