@@ -466,6 +466,9 @@ deriving instance Binary Raw
466deriving instance NFData Raw
466deriving instance NFData Raw
469+-- The type parameter `b` will normally be something like `TT Name` or just
470+-- `Raw`. We do not make a type-level distinction between TT terms that happen
471+-- to be TT types and TT terms that are not TT types.
469-- | All binding forms are represented in a unform fashion.
472-- | All binding forms are represented in a unform fashion.
470data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
473data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
471 | Pi { binderTy :: b }
474 | Pi { binderTy :: b }