{-# LANGUAGE MultiParamTypeClasses #-}

{-|
  Module:    HaskHOL.Core.Kernel.Types
  Copyright: (c) The University of Kansas 2013
  LICENSE:   BSD3

  Maintainer:  ecaustin@ittc.ku.edu
  Stability:   unstable
  Portability: unknown

  This module exports a safe view of HOL types for HaskHOL.  It also defines
  the primitive functions related to types.  For clarity, these functions have
  been seperated based on their influential system: HOL Light, Stateless HOL,
  and HOL2P.

  Note that, per the stateless approach, any stateful, but still primitive,
  functions related to types have been relocated to the "HaskHOL.Core.State"
  module.
-}
module HaskHOL.Core.Kernel.Types
    ( -- * A View of HOL Types
       -- ** A Quick Note on View Patterns
        -- $ViewPatterns
       -- ** A High-Level Overview of HOL Types
        -- $HOLTypes
      HOLType
    , HOLTypeView(..)
       -- ** A Quick Note on Type Variable Distinction
        -- $TypeDistinction
    , TypeOp
    , HOLTypeEnv
    , SubstTrip
      -- * HOL Light Type Primitives
       -- ** Alpha-Equivalence of Types
    , tyAlphaOrder -- :: HOLType -> HOLType -> Ordering
    , tyAConv      -- :: HOLType -> HOLType -> Bool
       -- ** Predicates, Constructors, and Destructors for Basic Types
    , isVarType   -- :: HOLType -> Bool
    , isType      -- :: HOLType -> Bool
    , mkVarType   -- :: String -> HOLType
    , destVarType -- :: HOLType -> Maybe String
    , destType    -- :: HOLType -> Maybe (String, [HOLType])
       -- ** Type Variable Extractors
    , tyVars    -- :: HOLType -> [HOLType]
    , catTyVars -- :: [HOLType] -> [HOLType]
       -- ** Type Substitution
    , TypeSubst
    , typeSubst     --  :: TypeSubst a b => [(a, b)] -> HOLType -> HOLType
    , typeSubstFull --  :: SubstTrip -> HOLType -> HOLType
       -- ** Commonly Used Types and Functions
    , tyBool    -- :: HOLType
    , tyA       -- :: HOLType
    , tyB       -- :: HOLType
    , destFunTy -- :: HOLType -> Maybe (HOLType, HOLType)
    , typeOf    -- :: HOLTerm -> HOLType
      -- * Stateless HOL Type Primitives
       -- ** Predicates, Constructors, and Destructors for Type Operators
    , isTypeOpVar   -- :: TypeOp -> Bool
    , newPrimTypeOp -- :: String -> Int -> TypeOp
    , mkTypeOpVar   -- :: String -> TypeOp
    , destTypeOp    -- :: TypeOp -> (String, Int)
       -- ** Commonly Used Type Operators
    , tyOpBool -- :: TypeOp
    , tyOpFun  -- :: TypeOp
    , tyApp    -- :: TypeOp -> [HOLType] -> Either String HOLType
       -- ** Type Operator Variable Extractors
    , typeOpVars    -- :: HOLType -> [TypeOp]
    , catTypeOpVars -- :: [HOLType] -> [TypeOp]
      -- * HOL2P Type Primitives
       -- ** Predicates, Constructors, and Destructors for Universal Types
    , isUType            -- :: HOLType -> Bool
    , isSmall            -- :: HOLType -> Bool
    , mkUType            -- :: HOLType -> HOLType -> Either String HOLType
    , mkUTypes           -- :: [HOLType] -> HOLType -> Either String HOLType
    , uTypeFromTypeOpVar -- :: TypeOp -> Int -> Either String HOLType
    , mkSmall            -- :: HOLType -> Either String HOLType
    , destUType          -- :: HOLType -> Maybe (HOLType, HOLType)
    , destUTypes         -- :: HOLType -> Maybe ([HOLType], HOLType)
       -- ** Commonly Used Functions
    , containsUType -- :: HOLType -> Bool
    , variantTyVar  -- :: [HOLType] -> HOLType -> HOLType
    , variantTyVars -- :: [HOLType] -> [HOLType] -> HOLType
    ) where

import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel.Prims

{- 
   HOL Light Type Primitives
   Note that the following primitives are in HaskHOL.Core.State as per 
   Stateless HOL:
   types, getTypeArityCtxt, getTypeArity, newType, mkType, mkFunTy
-}
-- | Provides an ordering for two types modulo alpha-equivalence.
tyAlphaOrder :: HOLType -> HOLType -> Ordering
tyAlphaOrder = tyorda []
  where tyorda :: HOLTypeEnv -> HOLType -> HOLType -> Ordering
        tyorda env ty1 ty2
            | ty1 == ty2 && all (uncurry (==)) env = EQ
            | otherwise =
                case (ty1, ty2) of
                  (TyVarIn{}, TyVarIn{}) -> alphavars env ty1 ty2
                  (TyAppIn tyop1 args1, TyAppIn tyop2 args2) ->
                      case compare tyop1 tyop2 of
                        EQ -> tyordas env args1 args2
                        res -> res
                  (UTypeIn v1 t1, UTypeIn v2 t2) -> 
                      tyorda ((v1, v2):env) t1 t2
                  (TyVarIn{}, _) -> LT
                  (_, TyVarIn{}) -> GT
                  (TyAppIn{}, _) -> LT
                  (_, TyAppIn{}) -> GT

        alphavars :: HOLTypeEnv -> HOLType -> HOLType -> Ordering
        alphavars [] ty1 ty2 = compare ty1 ty2
        alphavars ((t1, t2):oenv) ty1 ty2
            | ty1 == t1 = if ty2 == t2 then EQ else LT
            | otherwise = if ty2 == t2 then GT else alphavars oenv ty1 ty2

        tyordas :: HOLTypeEnv -> [HOLType] -> [HOLType] -> Ordering
        tyordas _ [] [] = EQ
        tyordas _ [] _ = LT
        tyordas _ _ [] = GT
        tyordas env (x:xs) (y:ys) =
            case tyorda env x y of
              EQ -> tyordas env xs ys
              res -> res

-- | Tests if two types are alpha-equivalent.
tyAConv :: HOLType -> HOLType -> Bool
tyAConv ty1 ty2 = tyAlphaOrder ty1 ty2 == EQ

-- | Predicate for type variables.
isVarType :: HOLType -> Bool
isVarType TyVarIn{} = True
isVarType _ = False

-- | Predicate for type applications
isType :: HOLType -> Bool
isType TyAppIn{} = True
isType _ = False

{-| 
  Constructs a type variable of a given name.  Note that the resultant type 
  variable is unconstrained.
-}
mkVarType :: String -> HOLType
mkVarType = TyVarIn False

{-| 
  Destructs a type variable, returning its name.  Fails with 'Nothing' if called
  on a non-variable type.
-}
destVarType :: HOLType -> Maybe String
destVarType (TyVarIn _ s) = Just s
destVarType _ = Nothing

{-| 
  Destructs a type application, returning its operator name and its list of type
  arguments.  Fails with 'Nothing' if called on a type that is not an 
  application.
-}
destType :: HOLType -> Maybe (TypeOp, [HOLType])
destType (TyAppIn op args) = Just (op, args)
destType _ = Nothing

{-| 
  Returns the list of all free, type variables in a type, not including type
  operator variables.
-}
tyVars :: HOLType -> [HOLType]
tyVars tv@TyVarIn{} = [tv]
tyVars (TyAppIn _ args) = catTyVars args
tyVars (UTypeIn tv ty) = tyVars ty \\ [tv]

{-| 
  Returns the list of all type variables in a list of types, not including type
  operator variables.
-}
catTyVars :: [HOLType] -> [HOLType]
catTyVars = foldr (union . tyVars) []

{-|
  The @TypeSubst@ class provides the framework for type substitution in HaskHOL.
  Note that, with the introduction of universal types and type operator
  variables, we now have three kinds of substitution to handle:

  * Substitution of types for type variables, satisfying type variable 
    constraints.

  * Instantiation of type operators with universal types.

  * Substitution of type operators for type operator variables.

  Rather than have three separate functions exposed to the user, we elected to
  provide a polymorphic type substitution function that will accept any
  well-formed, homogenous substitution environment.

  Note that the internals of @TypeSubst@ are hidden to prevent unsound
  re-definition.  The relevant type substitution function is re-exported as
  'typeSubst'.  We also provide a function, 'typeSubstFull', that
  accepts a triplet of all possible substitution environments that can be
  conveniently used in combination with 'typeMatch'.

  See the ITP2013 paper, "Stateless Higher-Order Logic with Quantified Types,"
  for more details.
-}
class TypeSubst a b where
    -- | Tests if a pair is a valid element in a substitution environment.
    validSubst :: (a, b) -> Bool
    {-| 
      Perfoms a type substitution as described above using the provided 
      environment.
    -}
    typeSubst' :: [(a, b)] -> HOLType -> HOLType

instance TypeSubst HOLType HOLType where
    validSubst (TyVarIn False _, _) = True
    validSubst (TyVarIn{}, ty) = isSmall ty
    validSubst _ = False
    typeSubst' = typeTypeSubst

instance TypeSubst TypeOp TypeOp where
    validSubst (_, TyOpVar{}) = False
    validSubst (TyOpVar{}, _) = True
    validSubst _ = False
    typeSubst' = typeOpSubst

instance TypeSubst TypeOp HOLType where
    validSubst (TyOpVar{}, UTypeIn{}) = True
    validSubst _ = False
    typeSubst' = typeOpInst

{-|
  Re-exports the internal type substitution function of the 'TypeSubst' class
  to prevent unsound re-definition.  Invalid substitution pairs are pruned from
  the environment such that substitution never fails.

  Note that the order of elements in a substitution pair follows the convention
  of most Haskell libraries, rather than the traditional HOL convention:
  
  * The second element is substituted for the first, i.e. the substitution pair
    @(tyA, tyBool)@ indicates that the boolean type should be substituted for
    the type variable @A@.
-}
{-# INLINEABLE typeSubst #-}
typeSubst :: TypeSubst a b => [(a, b)] -> HOLType -> HOLType
typeSubst = typeSubst'

{-| 
  A version of 'typeSubst' that accepts a triplet of type substitution 
  environments.
-}
typeSubstFull :: SubstTrip -> HOLType -> HOLType
typeSubstFull (tyenv, tyOps, opOps) =
    typeOpSubst opOps . typeOpInst tyOps . typeSubst' tyenv

-- Type subst for (HOLType, HOLType) pairs.
typeTypeSubst :: HOLTypeEnv -> HOLType -> HOLType
typeTypeSubst [] t = t
typeTypeSubst tyenv t =
    typeSubstRec (filter validSubst tyenv) t
  where typeSubstRec :: HOLTypeEnv -> HOLType -> HOLType
        typeSubstRec tyins ty@TyVarIn{} = assocd ty tyins ty
        typeSubstRec tyins (TyAppIn op args) =
            TyAppIn op $ map (typeSubstRec tyins) args
        typeSubstRec tyins ty@(UTypeIn tv tbody) =
            let tyins' = filter (\ (x, _) -> x /= tv) tyins in
              if null tyins' then ty
              -- test for name capture, renaming instances of tv if necessary
              else if any (\ (x, t') -> tv `elem` tyVars t' && 
                                        x `elem` tyVars tbody) tyins'
                   then let tvbs = tyVars tbody
                            tvpatts = map fst tyins'
                            tvrepls = catTyVars . mapMaybe (`lookup` tyins') $
                                        intersect tvbs tvpatts
                            tv' = variantTyVar ((tvbs \\ tvpatts) `union` 
                                                tvrepls) tv in
                          UTypeIn tv' $ typeSubstRec ((tv, tv') : tyins') tbody
                   else UTypeIn tv $ typeSubstRec tyins' tbody              
                                
-- | Alias to the primitive boolean type.
{-# INLINEABLE tyBool #-}
tyBool :: HOLType
tyBool = TyAppIn tyOpBool []

-- Used for error cases in type checking only.  Not exported.
{-# INLINEABLE tyBottom #-}
tyBottom :: HOLType
tyBottom = TyAppIn tyOpBottom []

-- | Alias to the unconstrained type variable @A@.
{-# INLINEABLE tyA #-}
tyA :: HOLType
tyA = TyVarIn False "A"

-- | Alias to the unconstrained type variable @B@.
{-# INLINEABLE tyB #-}
tyB :: HOLType
tyB = TyVarIn False "B"

{-| 
  Specialized version of 'destType' that returns the domain and range of a
  function type.  Fails with 'Nothing' if the type to be destructed isn't a
  primitive function type.
-}
destFunTy :: HOLType -> Maybe (HOLType, HOLType)
destFunTy (TyAppIn (TyPrim "fun" _) [ty1, ty2]) = Just (ty1, ty2)
destFunTy _ = Nothing

{-|
  Returns the type of term.  Fails with a special type, @tyBottom@, if the type
  is poorly constructed; this keeps the function total without requiring the
  use of an additional guard type like 'Maybe'.

  In practice, this type will never be seen provided the kernel is not modified
  to expose the internal constructors for terms.
-}
typeOf :: HOLTerm -> HOLType
typeOf (VarIn _ ty) = ty
typeOf (ConstIn _ ty _) = ty
typeOf (CombIn x _) =
    case destType $ typeOf x of
      Just (_, _ : ty : _) -> ty
      _ -> tyBottom
typeOf (AbsIn (VarIn _ ty) tm) =
    TyAppIn tyOpFun [ty, typeOf tm]
typeOf AbsIn{} = tyBottom
typeOf (TyAbsIn tv tb) = UTypeIn tv $ typeOf tb
typeOf (TyCombIn t ty) =
    case typeOf t of
      (UTypeIn tv tbody) -> typeSubst [(tv, ty)] tbody
      _ -> tyBottom

{-
   Stateless HOL Type Primitives
-}
-- | Predicate for type operator variables.
isTypeOpVar :: TypeOp -> Bool
isTypeOpVar TyOpVar{} = True
isTypeOpVar _ = False

{-| 
  Constructs a primitive type operator of a given name and arity.  Primitive
  type operators are used to represent constant, but undefined, types.
-}
newPrimTypeOp :: String -> Int -> TypeOp
newPrimTypeOp = TyPrim

{-|
  Constructs a type operator variable of a given name.  Note that type
  operator arities are not stored, only inferred from the context where the
  operator is used.

  The parser makes an attempt to guarantee that all instances of a type operator
  in a term have the same arity.  The same protection is not provided for terms
  that are manually constructed.
-}
mkTypeOpVar :: String -> TypeOp
mkTypeOpVar = TyOpVar

{-| 
  Destructs a type operator, returning its name and arity.  Note that we use -1 
  to indicate the arity of a type operator variable since that information is 
  not carried.
-}
destTypeOp :: TypeOp -> (String, Int)
destTypeOp (TyOpVar name) = (name, -1)
destTypeOp (TyPrim name arity) = (name, arity)
destTypeOp (TyDefined name arity _) = (name, arity)

-- | Alias to the primitive boolean type operator.
{-# INLINEABLE tyOpBool #-}
tyOpBool :: TypeOp
tyOpBool = TyPrim "bool" 0
-- Used for error cases in type checking only.  Not exported.
{-# INLINEABLE tyOpBottom #-}
tyOpBottom :: TypeOp
tyOpBottom = TyPrim "_|_" 0
-- | Alias to the primitive function type operator.
{-# INLINEABLE tyOpFun #-}
tyOpFun :: TypeOp
tyOpFun = TyPrim "fun" 2

{-|
  Constructs a type application from a provided type operator and list of type
  arguments.  Fails with 'Left' in the following cases:

  * A type operator variable is applied to zero arguments.

  * A type operator's arity disagrees with the length of the argument list.
-}
tyApp :: TypeOp -> [HOLType] -> Either String HOLType
tyApp tyOp@TyOpVar{} [] = 
    Left $ "tyApp: " ++ show tyOp ++ ": TyOpVar applied to zero args."
tyApp tyOp@TyOpVar{} args = Right $ TyAppIn tyOp args
tyApp tyOp args =
    let (_, arity) = destTypeOp tyOp in
      if arity == length args 
      then Right $ TyAppIn tyOp args
      else Left $ "tyApp: " ++ show tyOp ++ ": wrong number of arguments."

-- | Returns the list of all type operator variables in a type.
typeOpVars :: HOLType -> [TypeOp]
typeOpVars (TyAppIn op@TyOpVar{} args) = foldr (union . typeOpVars) [op] args
typeOpVars (UTypeIn _ tbody) = typeOpVars tbody
typeOpVars _ = []

-- | Returns the list of all type operator variables in a list of types.
catTypeOpVars :: [HOLType] -> [TypeOp]
catTypeOpVars = foldr (union . typeOpVars) []

-- substitution of type operator variables for other type operators.
-- Note that replacement with another type operator variable is allowed
typeOpSubst :: [(TypeOp, TypeOp)] -> HOLType -> HOLType
typeOpSubst [] t = t
typeOpSubst tyopenv t =
    tyOpSubstRec (filter validSubst tyopenv) t
  where tyOpSubstRec :: [(TypeOp, TypeOp)] -> HOLType -> HOLType
        tyOpSubstRec tyopins (TyAppIn op args) =
            let args' = map (tyOpSubstRec tyopins) args in
              case tryFind (\ (tp, tr) ->
                                if tp /= op ||
                                snd (destTypeOp tr) /= length args 
                                then Nothing
                                else Just tr) tyopins of
                Nothing -> TyAppIn op args'
                Just op' -> TyAppIn op' args'
        tyOpSubstRec tyopins (UTypeIn tv tbody) =
            UTypeIn tv $ tyOpSubstRec tyopins tbody
        tyOpSubstRec _ ty = ty

-- instantiation of type operator variables with universal types.
typeOpInst :: [(TypeOp, HOLType)] -> HOLType -> HOLType
typeOpInst [] t = t
typeOpInst tyopenv t = tyOpInstRec (filter validSubst tyopenv) t
  where arityOf :: HOLType -> Maybe Int
        arityOf ty = return (length . fst) <*> destUTypes ty      

        tyOpInstRec :: [(TypeOp, HOLType)] -> HOLType -> HOLType
        tyOpInstRec tyopins ty@(TyAppIn op args) =
            let args' = map (tyOpInstRec tyopins) args in
              case tryFind (\ (tp, tr) ->
                                if tp /= op || 
                                   arityOf tr /= (Just $ length args) 
                                then Nothing
                                else destUTypes tr) tyopins of
                Nothing -> TyAppIn op args'
                Just (rtvs, rtbody)
                    | isSmall rtbody -> typeSubst (zip rtvs args') rtbody
                    | otherwise -> ty
        tyOpInstRec tyopins (UTypeIn tv tbody) =
            if any (\ (x, ty) -> tv `elem` tyVars ty && 
                                 x `elem` typeOpVars tbody) tyopins
            -- test for name capture, renaming instances of tv if necessary 
            then let tvbs = typeOpVars tbody
                     tvpatts = map fst tyopins
                     tvrepls = catTyVars . mapMaybe (`lookup` tyopins) $
                                 intersect tvbs tvpatts
                     tv' = variantTyVar tvrepls tv in
                   UTypeIn tv' . tyOpInstRec tyopins $ 
                     typeSubst [(tv, tv')] tbody
            else UTypeIn tv $ tyOpInstRec tyopins tbody
        tyOpInstRec _ ty = ty
                  
                
{- 
   HOL2P Type Primitives
-}

-- | Predicate for universal types.
isUType :: HOLType -> Bool
isUType UTypeIn{} = True
isUType _ = False

{-|
  Predicate for small types.  Returns 'True' if all type variables in the type
  are constrained to be small and the type contains no universal types; returns 
  'False' otherwise. 
-}
isSmall :: HOLType -> Bool
isSmall (TyVarIn small _) = small
isSmall (TyAppIn _ args) = all isSmall args
isSmall UTypeIn{} = False

{-|
  Constructs a universal type of a given bound type and body type.  Fails with
  'Left' if the bound type is not a small, type variable.
-}
mkUType :: HOLType -> HOLType -> Either String HOLType
mkUType tv@(TyVarIn True _) tybody = Right $ UTypeIn tv tybody
mkUType _ _ = Left "mkUType"

{-|
  Constructs a compound universal type given a list of bound types and a body.    Fails with 'Left' if any internal call to 'mkUType' fails.
-}
mkUTypes :: [HOLType] -> HOLType -> Either String HOLType
mkUTypes = flip (foldrM mkUType)

{-|
  Constructs a compound universal type from a type operator variable and a given
  number of bound variables, i.e. 
  
  > uTypeFromTypeOpVar _T n === % 'A1 ... 'An. ('A1, ..., 'An)_T  

  Fails with 'Left' in the following cases:

  * @n<=0@ which would result in the application of a type operator to an
    empty list of type arguments.

  * The type operator argument is not a variable. 
-}
uTypeFromTypeOpVar :: TypeOp -> Int -> Either String HOLType
uTypeFromTypeOpVar s@TyOpVar{} n
    | n > 0 = 
        let tvs = map (\ x -> TyVarIn True $ 'A' : show x) [1 .. n] in
          mkUTypes tvs =<< tyApp s tvs
    | otherwise = 
        Left "uTypeFromTypeOpVar: must have a positive number of bound types."
uTypeFromTypeOpVar _ _ = 
    Left "uTypeFromTypeOpVar: type operator not a variable."

{-|
  Constructs a small type from a given type by constraining all of the type
  variables in the type to be small.  Fails with 'Left' if the type contains
  any universal types.
-}
mkSmall :: HOLType -> Either String HOLType
mkSmall (TyVarIn _ s) = Right $ TyVarIn True s
mkSmall (TyAppIn s tvs) = liftM (TyAppIn s) $ mapM mkSmall tvs
mkSmall UTypeIn{} = Left "mkSmall"

{-| 
  Destructs a universal type, returning its bound type and body type.  Fails
  with 'Nothing' if the provided type is not universally quantified.
-}
destUType :: HOLType -> Maybe (HOLType, HOLType)
destUType (UTypeIn tv ty) = Just (tv, ty)
destUType _ = Nothing

{-|
  Destructs a compound universal type, returning the list of bound variables
  and the final body type.  Fails if the provided type is not universally
  quantified.
-} 
destUTypes :: HOLType -> Maybe ([HOLType], HOLType)
destUTypes (UTypeIn tv tb) = Just $ destUTypesRec ([tv], tb)
  where destUTypesRec :: ([HOLType], HOLType) -> ([HOLType], HOLType)
        destUTypesRec (acc, UTypeIn tv' tb') = destUTypesRec (acc++[tv'], tb')
        destUTypesRec res = res
destUTypes _ = Nothing

-- | Predicate to test if a type contains a universal type at any level.
containsUType :: HOLType -> Bool
containsUType TyVarIn{} = False
containsUType (TyAppIn _ args) = any containsUType args
containsUType UTypeIn{} = True

{-|
  Renames a type variable to avoid sharing a name with any of a given list of
  type variables.  Note that this function is both smallness presserving and
  respecting.  Returns the original type if it's not a type variable.
-}
variantTyVar :: [HOLType] -> HOLType -> HOLType
variantTyVar avoid tv@(TyVarIn small name)
    | tv `elem` avoid = variantTyVar avoid . TyVarIn small $ name ++ "'"
    | otherwise = tv
variantTyVar _ ty = ty

{-|
  Renames a list of type variables to avoid sharing a name with any of a given
  list of type variables.  As each type variable is processed it is added to the
  list of avoids such that the resultant list of type variables are all uniquely
  named.
-}
variantTyVars :: [HOLType] -> [HOLType] -> [HOLType]
variantTyVars _ [] = []
variantTyVars avoid (tv:tvs) =
    let tv' = variantTyVar avoid tv in
      tv : variantTyVars (tv':avoid) tvs


-- Documentation copied from HaskHOL.Core.Prims

{-$ViewPatterns
  The primitive data types of HaskHOL are implemented using view patterns in
  order to simulate private data types:

  * Internal constructors are hidden to prevent manual construction of terms.

  * View constructors (those of 'HOLTypeView', 'HOLTermView', 'HOLThmView') are
    exposed to enable pattern matching. 

  * View patterns, as defined by instances of the 'view' function from the 
    @Viewable@ class, provide a conversion between the two sets of constructors.
-}

{-$HOLTypes
  The following data types combined provide the definition of HOL types in 
  HaskHOL.

  The primary data type, 'HOLType', follows closely from the 
  simply typed lambda calculus approach used in John Harrison's HOL Light 
  system. 

  There are two principle changes to Harrison's implementation:

  1.  Type operators have been introduced, via the 'TypeOp' data type, to 
      facilitate a stateless logical kernel following from Freek Wiedijk's 
      Stateless HOL system.

  2.  Universal types and type operator variables have been introduced to move
      the logic from simply typed to polymorphic following from Norbert 
      Voelker's HOL2P system.
-}

{-$TypeDistinction
  In order to keep HaskHOL's type system decidable, we follow the same 
  \"smallness\" constraint used by HOL2P: type variables that are constrained 
  to be small cannot be replaced with types that contain either universal types
  or unconstrained type variables.  This constraint, in addition to the
  restriction that universal types can only bind small type variables, prevents
  the system from performing a substitution that would result in a higher rank
  type than the system is capable of dealing with.  This effectively limits the
  type system to 2nd order polymorphism.

  Voelker elected to rely on syntactic distinction to differentiate between the
  many kinds of type variables (small, unconstrained, and operator); depending 
  on how it was to be used, the name of a variable was prepended with a special 
  symbol.  Internal to HaskHOL, we elected to replace these syntactic 
  distinctions with structural ones such that the following hold true:

  * @TyVarIn True \"x\"@ represents the small type variable \"\'x\"

  * @TyVarIn False \"x\"@ represents the unconstrainted type variable \"x\"

  * @TyOpVar \"x\"@ represents the type operator variable \"_x\"

  Note that external to HaskHOL, during I/O of terms, both the parser and
  pretty-printer still rely on the syntactic distinctions introduced by
  Voelker.
-}