Safe Haskell  SafeInferred 

 module DDC.Type.Exp
 data Exp a n
 = XVar !a !(Bound n)
  XCon !a !(DaCon n)
  XLAM !a !(Bind n) !(Exp a n)
  XLam !a !(Bind n) !(Exp a n)
  XApp !a !(Exp a n) !(Exp a n)
  XLet !a !(Lets a n) !(Exp a n)
  XCase !a !(Exp a n) ![Alt a n]
  XCast !a !(Cast a n) !(Exp a n)
  XType !a !(Type n)
  XWitness !a !(Witness a n)
  XDefix !a [Exp a n]
  XInfixOp !a String
  XInfixVar !a String
 data Lets a n
 data Alt a n = AAlt !(Pat n) !(Exp a n)
 data Pat n
 data Cast a n
 = CastWeakenEffect !(Effect n)
  CastPurify !(Witness a n)
  CastBox
  CastRun
 data Witness a n
 data DaCon n
 data WiCon n
 = WiConBuiltin !WbCon
  WiConBound !(Bound n) !(Type n)
 data WbCon
 = WbConPure
  WbConEmpty
  WbConUse
  WbConRead
  WbConAlloc
Documentation
module DDC.Type.Exp
Expressions
Welltyped expressions have types of kind Data
.
XVar !a !(Bound n)  Value variable or primitive operation. 
XCon !a !(DaCon n)  Data constructor or literal. 
XLAM !a !(Bind n) !(Exp a n)  Type abstraction (level1). 
XLam !a !(Bind n) !(Exp a n)  Value and Witness abstraction (level0). 
XApp !a !(Exp a n) !(Exp a n)  Application. 
XLet !a !(Lets a n) !(Exp a n)  Possibly recursive bindings. 
XCase !a !(Exp a n) ![Alt a n]  Case branching. 
XCast !a !(Cast a n) !(Exp a n)  Type cast. 
XType !a !(Type n)  Type can appear as the argument of an application. 
XWitness !a !(Witness a n)  Witness can appear as the argument of an application. 
XDefix !a [Exp a n]  Some expressions and infix operators that need to be resolved into proper function applications. 
XInfixOp !a String  Use of a naked infix operator, like in 1 + 2. INVARIANT: only appears in the list of an XDefix node. 
XInfixVar !a String  Use of an infix operator as a plain variable, like in (+) 1 2. INVARIANT: only appears in the list of an XDefix node. 
Possibly recursive bindings.
Case alternatives.
data Pat n
Pattern matching.
Type casts.
CastWeakenEffect !(Effect n)  Weaken the effect of an expression. The given effect is added to the effect of the body. 
CastPurify !(Witness a n)  Purify the effect (action) of an expression. 
CastBox  Box a computation, capturing its effects in the S computation type. 
CastRun  Run a computation, releasing its effects into the environment. 
Witnesses
data Witness a n
When a witness exists in the program it guarantees that a certain property of the program is true.
Data Constructors
data DaCon n
Data constructors.
DaConUnit  Baked in unit data constructor. 
DaConPrim  Primitive data constructor used for literals and bakedin constructors. The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor. 
DaConBound  Data constructor that has a data type declaration. 

Witness Constructors
data WiCon n
Witness constructors.
WiConBuiltin !WbCon  Witness constructors baked into the language. 
WiConBound !(Bound n) !(Type n)  Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed. 
data WbCon
Builtin witness constructors.
These are used to convert a runtime capability into a witness that the corresponding property is true.
WbConPure  (axiom) The pure effect is pure. pure :: Pure !0 
WbConEmpty  (axiom) The empty closure is empty. empty :: Empty $0 
WbConUse  Convert a capability guaranteeing that a region is in the global heap, into a witness that a closure using this region is empty. This lets us rely on the garbage collector to reclaim objects in the region. It is needed when we suspend the evaluation of expressions that have a region in their closure, because the type of the returned thunk may not reveal that it references objects in that region. use :: [r : %]. Global r => Empty (Use r) 
WbConRead  Convert a capability guaranteeing the constancy of a region, into a witness that a read from that region is pure. This lets us suspend applications that read constant objects, because it doesn't matter if the read is delayed, we'll always get the same result. read :: [r : %]. Const r => Pure (Read r) 
WbConAlloc  Convert a capability guaranteeing the constancy of a region, into a witness that allocation into that region is pure. This lets us increase the sharing of constant objects, because we can't tell constant objects of the same value apart. alloc :: [r : %]. Const r => Pure (Alloc r) 