The gist of ML modules

gist-ml.cabal

name:                gist-ml
version:             0.1.0.0
synopsis:            The gist of ML modules
-- description:         
license:             BSD3
author:              Aleksey Kliger
maintainer:          aleksey at lambdageek dot org
-- copyright:           
-- category:            
build-type:          Simple
-- extra-source-files:  
cabal-version:       >=1.10

library
  exposed-modules:
                       GistML
  -- other-modules:       
  -- other-extensions:    
  build-depends:       base >=4.6 && <4.7,
                       mtl >= 2.2,
                       unbound-generics
  -- hs-source-dirs:      
  default-language:    Haskell2010

GistML.hs

{-#
  LANGUAGE
    DeriveGeneric, DeriveDataTypeable,
    MultiParamTypeClasses,
    ViewPatterns
  #-}
-- A short example of an ML-style module system atop a core lambda calculus.
--
-- The core expression language has variables, applications and
-- lambdas and constants.  The type language has variables (of the single kind *)
-- and function types and some base types.
--
-- To this we add syntax for modules and signatures and expression and type level operations to
-- refer to projected fields of previously defined modules.
--
-- The signatures specify a series of specs.  Each spec may be: an abstract type declaration,
--  a manifest type alias, a value declared with its type, or a nested submodule declared with a
-- signature expression.  signature expressions are either literal signatures or the identifiers of
-- previously defined signaturs.
--
-- A model is a series of definitions.  Each definition may be: a manifest type alias,
-- a value defined to be equal to some expression, or a submodule defined by a module expression.
-- A module expression is either the path into a previously defined model, a literal module definition,
-- or a module expression sealed with a signature expression in order to hide some fields or to hide
-- the definitions of some types.
--
-- A toplevel program consists of a sequence of signature and module definitions.
--
-- Example:
--   signature S1 = { type t : * ; type s = t -> t ; val x : s}
--   signature S2 = { type t : * }
--   module M1 = { type t = Int ; type s = Int -> t}
--   module M2 = (M1 : S2)
module GistML where

import GHC.Generics (Generic)
import Data.Typeable (Typeable)

import Control.Applicative
import Control.Monad.Reader
import Control.Monad.Except
import qualified Data.List

import Unbound.Generics.LocallyNameless

-- ================================================================================
-- Part I: Syntax

-- Section 1 : Fields, Identifiers and Paths

-- A field is the "external" name for a component of a module.  It's
-- how other modules talk about each other's visible components.
type Field = String

-- An identifier is associated with a module, but
-- it substituted by paths.
type Ident = Name Path

-- A path picks out a submodule from the module associated with its
-- root ident.
data Path = Id Ident
          | Project Path Field
            deriving (Show, Generic, Typeable)

-- Signature identifiers are associated with signatures.  They're not
-- particularly interesting because they just form a flat namespace at the toplevel.
type SigIdent = Name SigPath

data SigPath = SigIdent SigIdent
             deriving (Show, Generic, Typeable)

-- Section 2 : Core language.

-- Variables stand for expressions.
type Var = Name Expr

-- A ValuePath is a Path (which picks out a module) together with a
-- Field that picks out a value component of that module.
data ValuePath = ValuePath Path Field
                 deriving (Show, Generic, Typeable)

data Expr =
  -- core language stuff
  V Var
  | I Integer
  | App Expr Expr
  | Lam (Bind (Var, Embed Type) Expr)
  -- reference to another module's values.
  | P ValuePath
  deriving (Show, Generic, Typeable)

-- Type variables stand for types.
type TyVar = Name Type

-- Pick out a type component of a module path.
data TypePath = TypePath Path Field
              deriving (Show, Generic, Typeable)

data Type =
  -- core language types
  TV TyVar
  | TInt
  | Arr Type Type
  -- refernce to another module's types
  | TP TypePath
  deriving (Show, Generic, Typeable)

-- Could have more kinds, but this simple example just has *
data Kind = KType
          deriving (Show, Generic, Typeable)

-- Section 3 : Signatures

-- A signature is like the type of a module.

-- One of the insights of the ML module system is that a signature is
-- like a record type {field1: ty1, ... fieldN: tyN} except that later
-- some of the fields may in fact be either abstract or manifest type
-- declarations, and later fields may depend on previous type fields.
-- To deal with this, each (type) field in a signature has both an extranal field name,
-- and an internal type variable that is bound in the rest of the signature.
-- There can also be nested submodules, in which case the external name is a field name,
-- and the internal 
data Sig
  =
    -- trivial empty signature
    NilSig
    -- { val f : T, sig }
  | ValSig Field Type Sig
    -- { type f : TypeSpec, a. Sig } where Sig may use "a" to refer to TypeSpec
  | TypeSig Field (Bind (TyVar, Embed TypeSpec) Sig)
    -- { module f : Sig2, id . Sig1 } where Sig1 may use "id" to refer to Sig2
  | SubmodSig Field (Bind (Ident, Embed SigExpr) Sig)
  deriving (Show, Generic, Typeable)

data TypeSpec
  =
    -- abstract type definition:   type f : *
    AbstractTypeSpec Kind
    -- manifest type alias:  type f : * = t
  | ManifestTypeSpec Kind Type
    -- other ways of making types would also go here.
  deriving (Show, Generic, Typeable)

-- SigExprs are the various sorts of things that a user can write in
-- places where we might want a signature.  Actually there are only
-- two things: SigIdents of previously defined signatures, or literal
-- Sigs.
data SigExpr = SigLit Sig
             | SigPath SigPath
             deriving (Show, Generic, Typeable)

-- Section 4: Modules

-- A module is a sequence of definitions in the same way that a
-- signature is a sequence of specifications.

data Mod
  =
    NilMod
    -- { val f : T = E, x . Mod} where Mod can refer to Expr by the name "x".
  | ValMod Field (Bind (Var, Embed Type, Embed Expr) Mod)
    -- { type f : * = T, a . Mod} within a module you have to define types,
    -- can't just declare them abstractly.
  | TypeMod Field (Bind (TyVar, Embed ManifestTypeDefn) Mod)
    -- { module f = Mod2, id . Mod1 }
  | SubmodMod Field (Bind (Ident, Embed ModExpr) Mod)
  deriving (Show, Generic, Typeable)

data ManifestTypeDefn
  = ManifestTypeDefn Kind Type
  deriving (Show, Generic, Typeable)

-- Again the user can write various sort of things in places where they ought to write a module.
data ModExpr
  =
    -- path of a previously defined module
    ModPath Path
    -- literal module contents
  | ModLit Mod
    -- generative sealing of a module with a signature.
    -- This is the principle means of data abstraction: by hiding the manfiest
    -- definitions of some type components, new abstract types may be created.
  | ModSeal ModExpr SigExpr
    -- if I added functors, functor application would go here.
  deriving (Show, Generic, Typeable)

-- Section 7 : Toplevel

-- stuff you can write in a file.  Basically a sequence of signature
-- and module definitions.

data Toplevel
  =
    -- eof
    TopNil
    -- signature s = SigExpr ; ...
  | TopSig (Bind (SigIdent, Embed SigExpr) Toplevel)
    -- module m = ModExpr ; ...
  | TopMod (Bind (Ident, Embed ModExpr) Toplevel)
  deriving (Show, Generic, Typeable)

-- ====================

-- Example

example :: Toplevel
example = let
  s2 = s2n "S2"
  m1 = s2n "M1"
  t = s2n "t"
  mkTop top = top TopNil
  mkSig si se = TopSig . bind (s2n si, embed se)
  mkMod mi me = TopMod . bind (s2n mi, embed me)
  seal m s = ModSeal m s
  mkTS f Nothing = TypeSig f . bind (s2n f, embed (AbstractTypeSpec KType))
  mkTS f (Just t') = TypeSig f . bind (s2n f, embed (ManifestTypeSpec KType t'))
  mkTM f t' = TypeMod f . bind (s2n f, embed (ManifestTypeDefn KType t'))
  sigLit se = SigLit (se NilSig)
  modLit me = ModLit (me NilMod)
  in
   mkTop
   $ mkSig "S1" (sigLit
                 $ mkTS "t" Nothing
                 . mkTS "s" (Just $ (TV t) `Arr` (TV t)))
   . mkSig "S2" (sigLit
                 $ mkTS "t" Nothing)
   . mkMod "M1" (modLit
                 $ mkTM "t" TInt
                 . mkTM "s" (TInt `Arr` (TV t)))
   . mkMod "M2" (seal (ModPath $ Id m1) (SigPath $ SigIdent s2))


--
-- > typecheck example
-- Right ()
--
typecheck :: Toplevel -> Either String ()
typecheck top = runFreshM $ runExceptT $ runReaderT (checkToplevel top) ([], [])


-- ==========
-- Interlude - let's implement alpha-equivalence and substitution for everything.

instance Alpha Toplevel

instance Alpha SigExpr
instance Alpha SigPath
instance Alpha Sig
instance Alpha TypeSpec
         
instance Alpha ModExpr
instance Alpha Path
instance Alpha Mod
instance Alpha ManifestTypeDefn

instance Alpha TypePath
instance Alpha ValuePath

instance Alpha Kind
instance Alpha Type
instance Alpha Expr

instance Subst Path Path
instance Subst Path SigPath
instance Subst Path SigExpr
instance Subst Path Sig
instance Subst Path TypeSpec
instance Subst Path Mod
instance Subst Path ModExpr
instance Subst Path ManifestTypeDefn

instance Subst Path TypePath
instance Subst Path ValuePath

instance Subst Path Kind
instance Subst Path Type
instance Subst Path Expr

instance Subst Type Sig
instance Subst Type SigPath
instance Subst Type SigExpr
instance Subst Type TypeSpec

instance Subst Type Mod
instance Subst Type ModExpr
instance Subst Type ManifestTypeDefn

instance Subst Type Kind

instance Subst Type Type
instance Subst Type TypePath
instance Subst Type Path

instance Subst Type Expr
instance Subst Type ValuePath

-- ================================================================================

-- Part II: Typechecking

-- In general, in order to typecheck we will use two contexts that I
-- will write D and G.  In D we will associate signature identifiers
-- with the signature that they stand for; module identifiers with the signature of that
-- module; and type variables with their type specs, where it's understood that bindings
-- that are added later may refer to everything in the context that comes earlier.
-- For example:   module M : sig type t1 : * end ; type a : * = t1.

-- We will represent contexts as lists of bindings and we will cons onto the front of the list
-- when we add the latest bindings.
type DCtx = [DBinding]

data DBinding
  =
    -- signature S = sig ... end
    DSig SigIdent Sig
    -- module M : sig ... end
  | DMod Ident Sig
    -- type a : *  or type a : * = t
  | DType TyVar TypeSpec

-- The term context is used when typechecking value definitions and
-- expressions it's just a list of types for every variable that's in
-- scope.
type GCtx = [(Var, Type)]

-- To typecheck we need the contexts and a source of fresh names
type TC = ReaderT (DCtx, GCtx) (ExceptT String FreshM)

-- Let's go in reverse.

-- To check a toplevel we check the signature or module and extend the context and continue.
checkToplevel :: Toplevel -> TC ()
checkToplevel TopNil = return ()
checkToplevel (TopSig bnd) = do
  ((sigId, unembed -> sigExpr), rest) <- unbind bnd
  sig <- checkSigExpr sigExpr
  local (extendD $ DSig sigId sig) $ checkToplevel rest
checkToplevel (TopMod bnd) = do
  ((modId, unembed -> modExpr), rest) <- unbind bnd
  sig <- checkModExpr modExpr
  local (extendD $ DMod modId sig) $ checkToplevel rest

-- To check a SigExpr, lookup the sig ident in the context, or check
-- a literal sig field by field
checkSigExpr :: SigExpr -> TC Sig
checkSigExpr (SigPath (SigIdent sigId)) = lookupSigId sigId
checkSigExpr (SigLit sig) = do
  checkSig sig
  return sig

-- Check that Sig is well formed by going through the fields in turn.
checkSig :: Sig -> TC ()
checkSig NilSig = return ()
checkSig (ValSig _f t sig) = do
  ensureType t KType -- t is the type of a value field, so it better have kind *
  checkSig sig
checkSig (TypeSig _f bnd) = do
  ((tyVar, unembed -> spec), rest) <- unbind bnd
  checkSpec spec
  local (extendD $ DType tyVar spec) $ checkSig rest
checkSig (SubmodSig _f bnd) = do
  ((subId, unembed -> sigExpr), rest) <- unbind bnd
  subSig <- checkSigExpr sigExpr
  local (extendD $ DMod subId subSig) $ checkSig rest

-- check that a type spec is well-formed.
checkSpec :: TypeSpec -> TC ()
checkSpec (AbstractTypeSpec _k) = return ()
checkSpec (ManifestTypeSpec k t) = ensureType t k

kindOfTypeSpec :: TypeSpec -> Kind
kindOfTypeSpec spec =
  case spec of
   AbstractTypeSpec k -> k
   ManifestTypeSpec k _ -> k

-- ensure that the given type is well formed and has a kind that is
-- equal to the given one.
ensureType :: Type -> Kind -> TC ()
ensureType t k = do
  k' <- checkType t
  unless (k `aeq` k')
    $ throwError ("expected type " ++ show t
                  ++ " to have kind " ++ show k
                  ++ " but got " ++ show k')

-- check a module expression and return its natural signature.  The
-- natural signature is the one you would read off from a literal
-- module.  For a sealed module, its natural signature is the one that
-- is ascribed to it.  For a module path its the embedding of its
-- strengthened signature into the Sig datatype (more on this
-- mysterious sentence later!)
checkModExpr :: ModExpr -> TC Sig
checkModExpr (ModLit modLit) = checkMod modLit
checkModExpr (ModSeal modExpr sigExpr) = do
  naturalSig <- checkModExpr modExpr
  -- check that the natural signature is at least as defined as the
  -- sealing sig.
  sealingSig <- checkSigExpr sigExpr
  naturalSig `subSigOf` sealingSig
  return sealingSig
checkModExpr (ModPath p) = do
  strongSig <- lookupModulePath p
  weakenStrong strongSig

-- check a module is well-formed and return its natural sig.
checkMod :: Mod -> TC Sig
checkMod NilMod = return NilSig
checkMod (ValMod f bnd) = do
  ((x, unembed -> ty, unembed -> e), rest) <- unbind bnd
  checkExpr e ty
  sigRest <- local (extendG $ (x, ty)) $ checkMod rest
  return $ ValSig f ty sigRest
checkMod (TypeMod f bnd) = do
  ((tyVar, unembed -> manifestTypeDefn), rest) <- unbind bnd
  spec <- checkManifestTypeDefn manifestTypeDefn
  sigRest <- local (extendD $ DType tyVar spec) $ checkMod rest
  return $ TypeSig f $ bind (tyVar, embed spec) sigRest
checkMod (SubmodMod f bnd) = do
  ((modId, unembed -> modExpr), rest) <- unbind bnd
  subSig <- checkModExpr modExpr
  sigRest <- local (extendD $ DMod modId subSig) $ checkMod rest
  return $ SubmodSig f $ bind (modId, embed (SigLit subSig)) sigRest

checkManifestTypeDefn :: ManifestTypeDefn -> TC TypeSpec
checkManifestTypeDefn (ManifestTypeDefn k t) = do
  ensureType t k
  return $ ManifestTypeSpec k t

-- ==========

-- So now we know how to typecheck modules and signatures, except:
-- 1. I have yet to tell you how to typecheck expressions and
-- kindcheck types.
-- 2. Also these mysterious "Strong signatures" showed up.
-- 3. I need to write the implementation of 'subSigOf'
-- 4. Various utilities for manipulating contexts.

-- Let's start with the core language checking.

checkExpr :: Expr -> Type -> TC ()
checkExpr e t = do
  -- In the language I showed so far, we can infer the type of every expression, so
  -- checking is just running inference and then ensuring that the resulting type
  -- is equivalent to the one we expected.
  t' <- inferExpr e
  isEq <- equivType t t'
  unless isEq
    $ throwError ("Expected the type of " ++ show e
                  ++ " to be " ++ show t
                  ++ " but got " ++ show t')

inferExpr :: Expr -> TC Type
inferExpr (V v) = lookupVar v
inferExpr (I _) = return TInt
inferExpr (App e1 e2) = do
  tArr <- inferExpr e1
  (tArg, tResult) <- ensureArrowTy tArr
  checkExpr e2 tArg
  return tResult
inferExpr (Lam bnd) = do
  ((x, unembed -> tArg), body) <- unbind bnd
  ensureType tArg KType
  tResult <- local (extendG (x, tArg)) $ inferExpr body
  return (Arr tArg tResult)
inferExpr (P valuePath) = lookupValuePath valuePath

checkType :: Type -> TC Kind
checkType (TV tyVar) = do
  spec <- lookupTyVar tyVar
  return $ kindOfTypeSpec spec
checkType TInt = return KType
checkType (Arr t1 t2) = do
  ensureType t1 KType
  ensureType t2 KType
  return KType
checkType (TP typePath) = kindOfTypeSpec <$> lookupTypePath typePath

ensureArrowTy :: Type -> TC (Type, Type)
ensureArrowTy t = do
  t' <- expandAliases t
  case t' of
   Arr dom cod -> return (dom, cod)
   _ -> throwError ("expected a function type, got " ++ show t)

equivType :: Type -> Type -> TC Bool
equivType t1 t2 = do
  t1' <- expandAliases t1
  t2' <- expandAliases t2
  return (t1' `aeq` t2')

-- ====================

-- Okay, okay, let's talk about the strong signatures.

-- So the idea here is that when we go to look up a value path (for
-- example) assuming that all the fields along the path exist and
-- actually end up picking out a particular value field with some type
-- we want to return a type that shares as many type equalities as
-- possible with the previous definitions in the modules along the
-- path.
--
-- Example:
--   module M1 : {
--      type t1 = Int
--      a1 . module M2 : {
--        type t2 : *
--        a2 . type t3 = a1 -> a2
--        a3 . val x : a3
--      }
--   }
--
-- (recall that each type field tX also has an internal name aX by
-- which later components of its containing module refer to it)
--
-- Now if we see 'M1.M2.x' we want to return "Int -> M1.M2.t2" That
-- is, although the natural type of x is either "a3" or "M1.M2.t3"
-- depending on your perspective, that wouldn't expose as much sharing
-- as possible.  (For example if there was a value y of type M1.t1 we
-- want to know that "x y" is a legal application -- that x has some
-- arrow type and that its domain is equivalent to the type of y).
--
-- So what we return instead is
--   {Int / a1} ({M1.M2.t2/a2} ({a1->a2 / a3} a3))
-- That is, as we traverse the module M1 to get to its M2
-- field, we substitute Int (the manifest rhs of t1) for a1 and
-- continue.  Then when we descend into M2 and see that t2 is
-- abstract, we substitute for the internal name a2, the "selfified"
-- name M1.M2.t2.  Finally when we go past t3, we replace a3 by the
-- rhs of the type alias, namely a1 -> a2 (which by now been transformed into Int -> M1.M2.t2).

-- An interesting property of carrying out this process to all of M1 is that dependencies among fields
-- disappear.  Instead we end up with
--   module M1 : {
--     type t1 = Int
--     module M2 : {
--       type t2 : *
--       type t3 = Int -> M1.M2.t2
--       val x : Int -> M1.M2.t2
--     }
--  }

-- We will call this non-dependent sort of signature a "strengthened" (or selfified) signature.
-- It warrants its own datatype

data SelfSig
  = NilSelfSig
  | ValSelfSig Field Type SelfSig
  | TypeSelfSig Field TypeSpec SelfSig
  | SubmodSelfSig Field SelfSig SelfSig -- first SelfSig is the
                                        -- selfified submodule, second
                                        -- is the rest of this sig.
  deriving Show

lookupModulePath :: Path -> TC SelfSig
lookupModulePath (Id modId) = do
  weakSig <- lookupModuleId modId
  strengthen (Id modId) weakSig
lookupModulePath (Project p f) = do
  strongSig <- lookupModulePath p
  projectModuleField strongSig f

lookupValuePath :: ValuePath -> TC Type
lookupValuePath (ValuePath p f) = do
  strongSig <- lookupModulePath p
  projectValueField strongSig f

lookupTypePath :: TypePath -> TC TypeSpec
lookupTypePath (TypePath p f) = do
  strongSig <- lookupModulePath p
  projectTypeField strongSig f

strengthen :: Path -> Sig -> TC SelfSig
strengthen _p NilSig = return NilSelfSig
strengthen p (ValSig f ty rest) = do
  strongRest <- strengthen p rest
  return (ValSelfSig f ty strongRest)
strengthen p (TypeSig f bnd) = do
  ((tyVar, unembed -> spec), rest) <- unbind bnd
  let
    self = TypePath p f
    rest' = subst tyVar (TP self) rest
  strongRest <- strengthen p rest'
  return (TypeSelfSig f spec strongRest)
strengthen p (SubmodSig f bnd) = do
  ((subId, unembed -> subSigExpr), rest) <- unbind bnd
  subSig <- checkSigExpr subSigExpr
  let
    self = Project p f
  strongSub <- strengthen self subSig
  let
    rest' = subst subId self rest
  strongRest <- strengthen p rest'
  return (SubmodSelfSig f strongSub strongRest)

-- the reverse operation.  Go from a SelfSig back to an ordinary Sig.
-- We need to pick some fresh names for the internal names of all the
-- components.  we use the freshness monad to pick them.  And of
-- course there won't be any references to them in the tail of the
-- signature because that's precisely the defining property of strong
-- sigs.
weakenStrong :: SelfSig -> TC Sig
weakenStrong NilSelfSig = return NilSig
weakenStrong (ValSelfSig f ty rest) = do
  weakRest <- weakenStrong rest
  return (ValSig f ty weakRest)
weakenStrong (TypeSelfSig f spec rest) = do
  weakRest <- weakenStrong rest
  tyvar <- fresh (hintFieldName f)
  return $ TypeSig f $ bind (tyvar, embed spec) weakRest
weakenStrong (SubmodSelfSig f subSelfSig rest) = do
  weakRest <- weakenStrong rest
  weakSub <- weakenStrong subSelfSig
  subId <- fresh (hintFieldName f)
  return $ SubmodSig f $ bind (subId, embed $ SigLit weakSub) weakRest

-- make up a name (probably stale) from a given field.
hintFieldName :: Field -> Name a
hintFieldName = s2n

-- Given a strong signature, find its submodel field with the given
-- name and return that submodel's strong signature.
projectModuleField :: SelfSig -> Field -> TC SelfSig
projectModuleField NilSelfSig f =
  throwError ("expected to find a submodule called " ++ f)
projectModuleField (ValSelfSig _ _ rest) f = projectModuleField rest f
projectModuleField (TypeSelfSig _ _ rest) f = projectModuleField rest f
projectModuleField (SubmodSelfSig f' subSig rest) f =
  if f == f' then return subSig else projectModuleField rest f

projectTypeField :: SelfSig -> Field -> TC TypeSpec
projectTypeField NilSelfSig f =
  throwError ("expected to find a type field called " ++ f)
projectTypeField (ValSelfSig _ _ rest) f = projectTypeField rest f
projectTypeField (TypeSelfSig f' spec rest) f =
  if f == f' then return spec else projectTypeField rest f
projectTypeField (SubmodSelfSig _ _ rest) f = projectTypeField rest f

projectValueField :: SelfSig -> Field -> TC Type
projectValueField NilSelfSig f =
  throwError ("expected to find a value field called " ++ f)
projectValueField (ValSelfSig f' ty rest) f =
  if f == f' then return ty else projectValueField rest f
projectValueField (TypeSelfSig _ _ rest) f = projectValueField rest f
projectValueField (SubmodSelfSig _ _ rest) f = projectValueField rest f

-- ========================================

-- subsignature

subSigOf :: Sig -> Sig -> TC ()
subSigOf _sig1 _sig2 = return () -- tedious to implement

-- ===========================================================================

-- utilities

lookupModuleId :: Ident -> TC Sig
lookupModuleId modId = do
  msig <- asks (findModule . fst)
  case msig of
   Just sig -> return sig
   Nothing -> throwError ("no module " ++ show modId)
  where
    findModule [] = Nothing
    findModule (DMod modId' sig : rest) =
      if modId == modId' then Just sig else findModule rest
    findModule (_ : rest) = findModule rest

lookupTyVar :: TyVar -> TC TypeSpec
lookupTyVar tv = do
  mspec <- asks (findTyVar . fst)
  case mspec of
   Just spec -> return spec
   Nothing -> throwError ("no type " ++ show tv)
  where
    findTyVar [] = Nothing
    findTyVar (DType tv' spec : rest) =
      if tv == tv' then Just spec else findTyVar rest
    findTyVar (_ : rest) = findTyVar rest

lookupSigId :: SigIdent -> TC Sig
lookupSigId sigIdent = do
  msig <- asks (findSig . fst)
  case msig of
   Just sig -> return sig
   Nothing -> throwError ("no signature identifier " ++ show sigIdent)
  where
    findSig [] = Nothing
    findSig (DSig sigIdent' sig : rest) =
      if sigIdent == sigIdent' then Just sig else findSig rest
    findSig (_ : rest) = findSig rest

lookupVar :: Var -> TC Type
lookupVar x = do
  mt <- asks (Data.List.lookup x . snd)
  case mt of
   Just t -> return t
   Nothing -> throwError ("no variable " ++ show x)
  
extendD :: DBinding -> (DCtx, GCtx) -> (DCtx, GCtx)
extendD b (d, g) = (b : d, g)

extendG :: (Var,  Type) -> (DCtx, GCtx) -> (DCtx, GCtx)
extendG b (d, g) = (d, b:g)

--------------------

expandAliases :: Type -> TC Type
expandAliases (Arr t1 t2) = Arr <$> expandAliases t1 <*> expandAliases t2
expandAliases t@TInt = return t
expandAliases t@(TV a) = do
  spec <- lookupTyVar a
  case spec of
   ManifestTypeSpec _ t' -> expandAliases t'
   _ -> return t
expandAliases t@(TP p) = do
  spec <- lookupTypePath p
  case spec of
   ManifestTypeSpec _ t' -> return t'
   _ -> return t

References

1. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher order modules with sharing. POPL 1994.
2. Robert Harper and Chris Stone. A type-theoretic interpretation of Standard ML.
   In Proof, Language and Interaction: Essays in Honour of Robin Milner. The MIT
   Press, 2000. Extended version published as CMU technical report CMU-CS-97-147.
3. Xavier Leroy. A modular module system. Journal of Functional Programming, Volume 10 Issue 3, May 2000.
4. Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. ICFP 2011.