@@ -472,19 +472,19 @@ deriving instance NFData Raw
472472!-}
473473
474474-- | All binding forms are represented in a unform fashion.
475−data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
476− | Pi { binderTy :: b }
477− | Let { binderTy :: b,
475+data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
476+ | Pi { binderTy :: !b }
477+ | Let { binderTy :: !b,
478478 binderVal :: b {-^ value for bound variable-}}
479− | NLet { binderTy :: b,
479+ | NLet { binderTy :: !b,
480480 binderVal :: b }
481− | Hole { binderTy :: b}
481+ | Hole { binderTy :: !b}
482482 | GHole { envlen :: Int,
483− binderTy :: b}
484− | Guess { binderTy :: b,
483+ binderTy :: !b}
484+ | Guess { binderTy :: !b,
485485 binderVal :: b }
486− | PVar { binderTy :: b }
487− | PVTy { binderTy :: b }
486+ | PVar { binderTy :: !b }
487+ | PVTy { binderTy :: !b }
488488 deriving (Show, Eq, Ord, Functor)
489489{-!
490490deriving instance Binary Binder
@@ -586,8 +586,8 @@ instance Eq NameType where
586586-- | Terms in the core language
587587data TT n = P NameType n (TT n) -- ^ named references
588588 | V !Int -- ^ a resolved de Bruijn-indexed variable
589− | Bind n (Binder (TT n)) (TT n) -- ^ a binding
590− | App (TT n) (TT n) -- ^ function, function type, arg
589+ | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
590+ | App !(TT n) (TT n) -- ^ function, function type, arg
591591 | Constant Const -- ^ constant
592592 | Proj (TT n) !Int -- ^ argument projection; runtime only
593593 -- (-1) is a special case for 'subtract one from BI'