diff --git a/Language/Symantic/Compiling/Beta.hs b/Language/Symantic/Compiling/Beta.hs
--- a/Language/Symantic/Compiling/Beta.hs
+++ b/Language/Symantic/Compiling/Beta.hs
@@ -11,12 +11,12 @@
 -- | Term application: apply second given 'TermT' to the first,
 -- applying embedded 'TeSym's, or return an error.
 betaTerm ::
- forall src ss es vs fun arg.
+ forall src ss ts vs fun arg.
  SourceInj (TypeVT src) src =>
  Constable (->) =>
- Term src ss es vs (fun::K.Type) ->
- Term src ss es vs (arg::K.Type) ->
- Either (Error_Beta src) (TermT src ss es vs)
+ Term src ss ts vs (fun::K.Type) ->
+ Term src ss ts vs (arg::K.Type) ->
+ Either (Error_Beta src) (TermT src ss ts vs)
 betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
 	case tf of
 	 TyApp _ (TyApp _ a2b a2b_a) a2b_b
@@ -41,8 +41,8 @@
 betaTerms ::
  SourceInj (TypeVT src) src =>
  Constable (->) =>
- BinTree (TermVT src ss es) ->
- Either (Error_Beta src) (TermVT src ss es)
+ BinTree (TermVT src ss ts) ->
+ Either (Error_Beta src) (TermVT src ss ts)
 betaTerms t =
 	collapseBT (\acc ele -> do
 		TermVT (Term qf tf te_fun) <- acc
@@ -61,8 +61,10 @@
 			let tf'' = subst mgu tf'
 			let ta'' = subst mgu ta'
 			TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
-			normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
+			normalizeVarsTy (qr #> tr) $ \case
+			 TyApp _ (TyApp _ _c qr') tr' ->
 				Right $ TermVT $ Term qr' tr' te_res
+			 _ -> undefined -- FIXME: as of GHC 8.2, GHC is no longer clever enough to rule out other cases
 	 ) (Right <$> t)
 
 -- * Type 'Error_Beta'
diff --git a/Language/Symantic/Compiling/Grammar.hs b/Language/Symantic/Compiling/Grammar.hs
--- a/Language/Symantic/Compiling/Grammar.hs
+++ b/Language/Symantic/Compiling/Grammar.hs
@@ -10,7 +10,7 @@
 import Control.Monad (void)
 import Data.Semigroup (Semigroup(..))
 import Data.Map.Strict (Map)
-import Prelude hiding (mod, not, any)
+import Prelude hiding (any)
 import qualified Data.Function as Fun
 import qualified Data.Map.Strict as Map
 import qualified Data.Text as Text
@@ -21,7 +21,7 @@
 
 -- * Class 'Gram_Term_Name'
 class
- ( Gram_Terminal g
+ ( Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_Try g
@@ -54,7 +54,7 @@
 		(NameTe . Text.pack <$>) $
 		(identG `minus`) $
 		Fun.const
-		 <$> g_NameTeKey
+		 <$> g_NameTeIdKey
 		 <*. (any `but` g_NameTeIdTail)
 		where
 		identG = (:) <$> headG <*> many (cfOf g_NameTeIdTail)
@@ -63,8 +63,8 @@
 	g_NameTeIdTail = rule "NameTeIdTail" $
 		unicat Unicat_Letter <+>
 		unicat Unicat_Number
-	g_NameTeKey :: Reg rl g String
-	g_NameTeKey = rule "NameTeKey" $
+	g_NameTeIdKey :: Reg rl g String
+	g_NameTeIdKey = rule "NameTeIdKey" $
 		choice $ string <$> ["in", "let"]
 	
 	g_ModNameTeOp :: CF g (Mod NameTe)
@@ -77,7 +77,7 @@
 		(NameTe . Text.pack <$>) $
 		(some (cfOf g_NameTeOpOk) `minus`) $
 		Fun.const
-		 <$> g_NameTeKeySym
+		 <$> g_NameTeOpKey
 		 <*. (any `but` g_NameTeOpOk)
 	g_NameTeOpOk :: Terminal g Char
 	g_NameTeOpOk = rule "NameTeOpOk" $
@@ -88,8 +88,8 @@
 		 ]) `but` koG
 		where
 		koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])
-	g_NameTeKeySym :: Reg rl g String
-	g_NameTeKeySym = rule "NameTeKeySym" $
+	g_NameTeOpKey :: Reg rl g String
+	g_NameTeOpKey = rule "NameTeOpKey" $
 		choice $ string <$> ["\\", "->", "=", "@"]
 
 deriving instance Gram_Term_Name g => Gram_Term_Name (CF g)
@@ -98,7 +98,7 @@
 
 -- * Class 'Gram_Term_Type'
 class
- ( Gram_Terminal g
+ ( Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_AltApp g
@@ -109,7 +109,7 @@
  , Gram_Type src g
  ) => Gram_Term_Type src g where
 	g_term_abst_decl :: CF g (NameTe, AST_Type src)
-	g_term_abst_decl = rule "term_abst_decl" $
+	g_term_abst_decl = rule "TermAbstDecl" $
 		parens $ (,)
 		 <$> g_NameTe
 		 <*  (symbol "::" <+> symbol ":")
@@ -145,7 +145,7 @@
 class
  ( Gram_Source src g
  , Gram_Error Error_Term_Gram g
- , Gram_Terminal g
+ , Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_App g
@@ -159,14 +159,14 @@
  , Gram_State (Imports NameTe, Modules src ss) g
  ) => Gram_Term src ss g where
 	g_term :: CF g (AST_Term src ss)
-	g_term = rule "term" $
+	g_term = rule "Term" $
 		choice
 		 [ try g_term_abst
 		 , g_term_operators
 		 , g_term_let
 		 ]
 	g_term_operators :: CF g  (AST_Term src ss)
-	g_term_operators = rule "term_operators" $
+	g_term_operators = rule "TermOperators" $
 		G.catch $
 		left Error_Term_Gram_Fixity <$>
 		g_ops
@@ -174,29 +174,30 @@
 		g_ops :: CF g (Either Error_Fixity  (AST_Term src ss))
 		g_ops = operators g_term_atom g_prefix g_infix g_postfix
 		g_prefix  :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
-		g_infix   :: CF g (Infix,  AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
 		g_postfix :: CF g (Unifix, AST_Term src ss -> AST_Term src ss)
-		g_prefix  = G.catch $ G.source $ G.getAfter $ op_prefix  <$> g_prefix_op
-		g_infix   = G.catch $ G.source $ G.getAfter $ op_infix   <$> g_infix_op
-		g_postfix = G.catch $ G.source $ G.getAfter $ op_postfix <$> g_postfix_op
-		op_infix
-		 :: Mod NameTe
-		 -> (Imports NameTe, Modules src ss)
-		 -> src
-		 -> Either Error_Term_Gram
-		           (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
+		g_infix, g_app :: CF g (Infix,  AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
+		g_app     = rule "TermApp"     $ G.source $ op_app <$> pure ()
+		g_prefix  = rule "TermPrefix"  $ G.catch $ G.source $ G.getAfter $ op_prefix  <$> g_op_prefix
+		g_postfix = rule "TermPostfix" $ G.catch $ G.source $ G.getAfter $ op_postfix <$> g_op_postfix
+		g_infix   = rule "TermInfix"   $ try (G.catch $ G.source $ G.getAfter $ op_infix <$> g_op_infix) <+> g_app
+		op_app :: () -> src -> (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
+		op_app () src =
+			(Infix (Just AssocL) 9,) $ \a b ->
+				(BinTree0 (Token_Term_App src) `BinTree2` a) `BinTree2` b
+		op_infix :: Mod NameTe -> (Imports NameTe, Modules src ss) -> src ->
+		 Either Error_Term_Gram
+		        (Infix, AST_Term src ss -> AST_Term src ss -> AST_Term src ss)
 		op_infix name (imps, mods) src = do
 			t <- Error_Term_Gram_Module `left`
 				lookupDefTerm FixyInfix imps name mods
 			Right $ (token_fixity t,) $ \a b ->
 				(BinTree0 (token_term t src) `BinTree2` a) `BinTree2` b
-		op_prefix, op_postfix
-		 :: Mod NameTe
-		 -> (Imports NameTe, Modules src ss)
-		 -> src
-		 -> Either Error_Term_Gram
-		           ( Unifix
-		           , AST_Term src ss -> AST_Term src ss )
+		op_prefix, op_postfix ::
+		 Mod NameTe ->
+		 (Imports NameTe, Modules src ss) ->
+		 src ->
+		 Either Error_Term_Gram
+		        (Unifix, AST_Term src ss -> AST_Term src ss)
 		op_prefix name (imps, mods) src = do
 			t <- Error_Term_Gram_Module `left`
 				lookupDefTerm FixyPrefix imps name mods
@@ -207,27 +208,27 @@
 				lookupDefTerm FixyPostfix imps name mods
 			Right $ (token_fixity t,) $ \a ->
 				BinTree0 (token_term t src) `BinTree2` a
-		g_postfix_op :: CF g (Mod NameTe)
-		g_postfix_op = rule "term_op_postfix" $
+		g_op_postfix :: CF g (Mod NameTe)
+		g_op_postfix = rule "TermOpPostfix" $
 			lexeme $
 				g_backquote *> g_ModNameTeId <+> -- <* (G.cfOf $ Gram.Term (pure ' ') `but` g_backquote)
 				g_ModNameTeOp
-		g_infix_op :: CF g (Mod NameTe)
-		g_infix_op = rule "term_op_infix" $
+		g_op_infix :: CF g (Mod NameTe)
+		g_op_infix = rule "TermOpInfix" $
 			lexeme $
 				between g_backquote g_backquote g_ModNameTeId <+>
-				try (Fun.const <$> g_ModNameTeOp <*> (string " " <+> string "\n")) <+>
+				try g_ModNameTeOp <+>
 				pure (Mod [] " ")
-		g_prefix_op :: CF g (Mod NameTe)
-		g_prefix_op = rule "term_op_prefix" $
+		g_op_prefix :: CF g (Mod NameTe)
+		g_op_prefix = rule "TermOpPrefix" $
 			lexeme $
 				g_ModNameTeId <* g_backquote <+>
 				g_ModNameTeOp
-		g_backquote :: Gram_Terminal g' => g' Char
+		g_backquote :: Gram_Char g' => g' Char
 		g_backquote = char '`'
 	
 	g_term_atom :: CF g  (AST_Term src ss)
-	g_term_atom = rule "term_atom" $
+	g_term_atom = rule "TermAtom" $
 		choice $
 		 {-(try (
 			G.source $
@@ -235,8 +236,7 @@
 			 <$ char '@' <*> g_type) :) $
 		 -}
 		 (try <$> g_term_atomsR @_ @_ @ss) <>
-		 [ try $
-			G.catch $ G.source $ G.getAfter $
+		 [ try $ G.catch $ G.source $ G.getAfter $
 			(\m (imps, mods) src ->
 				case lookupDefTerm FixyInfix imps m mods of
 				 Right t -> Right $ BinTree0 $ token_term t src
@@ -248,9 +248,9 @@
 		 , g_term_group
 		 ]
 	g_term_group :: CF g (AST_Term src ss)
-	g_term_group = rule "term_group" $ parens g_term
+	g_term_group = rule "TermGroup" $ parens g_term
 	g_term_abst :: CF g (AST_Term src ss)
-	g_term_abst = rule "term_abst" $
+	g_term_abst = rule "TermAbst" $
 		G.source $
 		((\(xs, te) src ->
 			foldr (\(x, ty_x) ->
@@ -294,7 +294,7 @@
 			 , token_fixity = infixN5
 			 }
 	g_term_let :: CF g  (AST_Term src ss)
-	g_term_let = rule "term_let" $
+	g_term_let = rule "TermLet" $
 		G.source $
 		(\name args bound body src ->
 			BinTree0 $
@@ -365,11 +365,11 @@
  , void g_NameTe
  , void g_NameTeId
  , void $ G.cfOf g_NameTeIdTail
- , void $ G.cfOf g_NameTeKey
+ , void $ G.cfOf g_NameTeIdKey
  , void g_ModNameTeOp
  , void g_NameTeOp
  , void $ G.cfOf g_NameTeOpOk
- , void $ G.cfOf g_NameTeKeySym
+ , void $ G.cfOf g_NameTeOpKey
  ] where
 	voiD :: CF g (AST_Term () '[Proxy (->), Proxy Integer]) -> CF g ()
 	voiD = (() <$)
diff --git a/Language/Symantic/Compiling/Module.hs b/Language/Symantic/Compiling/Module.hs
--- a/Language/Symantic/Compiling/Module.hs
+++ b/Language/Symantic/Compiling/Module.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Language.Symantic.Compiling.Module where
@@ -13,7 +12,7 @@
 import Data.Semigroup (Semigroup(..))
 import Data.Set (Set)
 import Data.String (IsString(..))
-import Prelude hiding (mod, not, any)
+import Prelude hiding (mod, not)
 import qualified Data.Map.Strict as Map
 
 import Language.Symantic.Grammar
diff --git a/Language/Symantic/Compiling/Term.hs b/Language/Symantic/Compiling/Term.hs
--- a/Language/Symantic/Compiling/Term.hs
+++ b/Language/Symantic/Compiling/Term.hs
@@ -165,7 +165,7 @@
 infixr 5 `CtxTeS`
 
 -- ** Type 'TermDef'
--- | Convenient type alias for defining 'Term'.
+-- | Convenient type alias to define a 'Term'.
 type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
 
 -- ** Type family 'Sym'
diff --git a/Language/Symantic/Interpreting/View.hs b/Language/Symantic/Interpreting/View.hs
--- a/Language/Symantic/Interpreting/View.hs
+++ b/Language/Symantic/Interpreting/View.hs
@@ -13,10 +13,10 @@
 -- | Interpreter's data.
 newtype View a
  =      View
- {    unView -- Inherited attribuctx:
+ {    unView -- Inherited attributes:
              :: (Infix, Side)
              -> DepthLam
-             -- Synthetised attribuctx:
+             -- Synthetised attributes:
              -> Text
  }
 type DepthLam = Int
diff --git a/Language/Symantic/Typing/Document.hs b/Language/Symantic/Typing/Document.hs
--- a/Language/Symantic/Typing/Document.hs
+++ b/Language/Symantic/Typing/Document.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Typing.Document where
 
@@ -54,8 +55,8 @@
 	go v2n (infixB SideL pr, SideL) ty
 	where
 	go ::
-	 forall x.
-	 (Map IndexVar Name) -> -- names of variables
+	 forall kx (x::kx).
+	 Map IndexVar Name -> -- names of variables
 	 (Infix, Side) ->
 	 Type src vs x -> d
 	-- Var
diff --git a/Language/Symantic/Typing/Grammar.hs b/Language/Symantic/Typing/Grammar.hs
--- a/Language/Symantic/Typing/Grammar.hs
+++ b/Language/Symantic/Typing/Grammar.hs
@@ -11,7 +11,6 @@
 import Data.Maybe (fromMaybe)
 import Data.Semigroup (Semigroup(..))
 import Data.String (IsString(..))
-import Prelude hiding (any)
 import qualified Data.Char as Char
 import qualified Data.Map.Strict as Map
 import qualified Data.Text as Text
@@ -96,7 +95,7 @@
 
 -- * Class 'Gram_Mod'
 class
- ( Gram_Terminal g
+ ( Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_Try g
@@ -130,7 +129,7 @@
 
 -- * Class 'Gram_Type_Name'
 class
- ( Gram_Terminal g
+ ( Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_Try g
@@ -189,7 +188,7 @@
 -- | Read an 'AST_Type' from a textual source.
 class
  ( Gram_Source src g
- , Gram_Terminal g
+ , Gram_Char g
  , Gram_Rule g
  , Gram_Alt g
  , Gram_Try g
@@ -206,14 +205,14 @@
  , Constable (,)
  ) => Gram_Type src g where
 	g_type :: CF g (AST_Type src)
-	g_type = rule "type" $ g_type_fun
+	g_type = rule "Type" $ g_type_fun
 	g_type_fun :: CF g (AST_Type src)
-	g_type_fun = rule "type_fun" $
+	g_type_fun = rule "TypeFun" $
 		infixrG g_type_list (source $ op <$ symbol "->")
 		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(->) src)
 	-- TODO: maybe not harcoding g_type_list and g_type_tuple2
 	g_type_list :: CF g (AST_Type src)
-	g_type_list = rule "type_list" $
+	g_type_list = rule "TypeList" $
 		source $ inside mk
 		 (symbol "[") (optional g_type) (symbol "]")
 		 (const <$> g_type_tuple2)
@@ -222,24 +221,24 @@
 		mk (Just a) src = BinTree2 (tok src) a
 		tok = BinTree0 . Token_Type_Const . typeTLen @[]
 	g_type_tuple2 :: CF g (AST_Type src)
-	g_type_tuple2 = rule "type_tuple2" $
+	g_type_tuple2 = rule "TypeTuple2" $
 		try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
 		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(,) src)
 	g_type_app :: CF g (AST_Type src)
-	g_type_app = rule "type_app" $
+	g_type_app = rule "TypeApp" $
 		foldl1' BinTree2 <$> some (g_type_atom)
 	g_type_atom :: CF g (AST_Type src)
-	g_type_atom = rule "type_atom" $
+	g_type_atom = rule "TypeAtom" $
 		try (parens g_type) <+>
-		g_type_name_const <+>
-		g_type_name_var
-	g_type_name_const :: CF g (AST_Type src)
-	g_type_name_const = rule "type_name_const" $
+		g_type_const <+>
+		g_type_var
+	g_type_const :: CF g (AST_Type src)
+	g_type_const = rule "TypeConst" $
 		lexeme $ catch $ source $ getBefore $
 		(\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
 		 <$> g_ModNameTy
-	g_type_name_var :: CF g (AST_Type src)
-	g_type_name_var = rule "type_name_var" $
+	g_type_var :: CF g (AST_Type src)
+	g_type_var = rule "TypeVar" $
 		lexeme $ source $
 		(\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
 		 <$> unicat (Unicat Char.LowercaseLetter)
@@ -292,7 +291,7 @@
  , g_type_tuple2
  , g_type_app
  , g_type_atom
- , g_type_name_const
- , g_type_name_var
+ , g_type_const
+ , g_type_var
  -- , g_type_symbol
  ]
diff --git a/Language/Symantic/Typing/Peano.hs b/Language/Symantic/Typing/Peano.hs
--- a/Language/Symantic/Typing/Peano.hs
+++ b/Language/Symantic/Typing/Peano.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE GADTs #-}
-{-# OPTIONS_GHC -fno-warn-missing-methods #-}
 -- | Natural numbers inductivey defined at the type-level, and of kind @*@.
 module Language.Symantic.Typing.Peano where
 
diff --git a/Language/Symantic/Typing/Type.hs b/Language/Symantic/Typing/Type.hs
--- a/Language/Symantic/Typing/Type.hs
+++ b/Language/Symantic/Typing/Type.hs
@@ -1,11 +1,13 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
-{-# language ConstraintKinds #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
 module Language.Symantic.Typing.Type
  ( module Language.Symantic.Typing.Type
  , Proxy(..)
@@ -59,6 +61,11 @@
 	            -> Type (x #~ y) src vs
 	-}
 
+pattern a :$ b <- TyApp _ a b
+infixr 0 :$
+pattern a :@ b <- TyApp _ a b
+infixl 9 :@
+
 instance Source src => Eq (Type src vs t) where
 	x == y = isJust $ eqType x y
 instance SourceInj (TypeVT src) src => TestEquality (Type src vs) where
@@ -720,7 +727,7 @@
 kindOfType (TyVar _src _n v)         = kindOfVar v
 kindOfType (TyFam _src _len fam _as) = kindOfConst fam
 
--- | Remove unused 'Var's from ther context.
+-- | Remove unused 'Var's from the context.
 normalizeVarsTy ::
  Type src vs (t::kt) ->
  (forall vs'. Type src vs' (t::kt) -> ret) -> ret
diff --git a/Language/Symantic/Typing/Unify.hs b/Language/Symantic/Typing/Unify.hs
--- a/Language/Symantic/Typing/Unify.hs
+++ b/Language/Symantic/Typing/Unify.hs
@@ -146,7 +146,7 @@
  (TypeT src vs, [TypeT src vs])
 spineTy typ = go [] typ
 	where
-	go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
+	go :: forall kx (x::kx). [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
 	go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
 	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
 	 = go ctx t -- NOTE: skip the constraint @q@.
diff --git a/Language/Symantic/Typing/Variable.hs b/Language/Symantic/Typing/Variable.hs
--- a/Language/Symantic/Typing/Variable.hs
+++ b/Language/Symantic/Typing/Variable.hs
@@ -9,17 +9,12 @@
 import Data.Proxy (Proxy(..))
 import Data.String (IsString(..))
 import Data.Text (Text)
-import Data.Type.Equality ((:~:)(..))
+import Data.Type.Equality ((:~:)(..), (:~~:)(..))
 import qualified Data.Kind as K
 
 import Language.Symantic.Grammar
 import Language.Symantic.Typing.List
 import Language.Symantic.Typing.Kind
-
--- | /Heterogeneous propositional equality/:
--- like (:~:) but prove also that the kinds are equal.
-data (:~~:) (a::ka) (b::kb) where
-	HRefl :: a :~~: a
 
 -- * Type 'Var'
 -- | A /type variable/, indexed amongst a type-level list.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -65,14 +65,12 @@
 
 # Usage
 
-Please pick in [symantic-lib](https://hackage.haskell.org/package/symantic-lib)
-a few specific `Lib/*.hs` files near what you want to do
-and the corresponding `Lib/*/Test.hs` file,
-if any in the [Git repository](git://git.autogeree.net/symantic),
-to learn by examples how to use this library.
+Please learn how to use this library by reading example source files in `test/`
+in [symantic-lib](https://hackage.haskell.org/package/symantic-lib)
+in [Git repository](git://git.autogeree.net/symantic).
 
-Those `Lib/*/Test.hs` files use [megaparsec](https://hackage.haskell.org/package/megaparsec) as parser
-(see `Grammar/Megaparsec.hs`) and a default grammar somehow sticking to Haskell's,
+These `test` files use [megaparsec](https://hackage.haskell.org/package/megaparsec) as parser
+(see `test/Testing/Megaparsec.hs`) and a default grammar somehow sticking to Haskell's,
 but staying context-free (so in particular: insensitive to the indentation),
 and supporting prefix and postfix operators.
 This grammar — itself written as a symantic embedded DSL
@@ -157,7 +155,7 @@
 * `PolyKinds` for avoiding a lot of uses of `Proxy`.
 * `Rank2Types` or `ExistentialQuantification` for parsing `GADT`s.
 * `TypeApplications` for having a more concise syntax
-  to build `Type` (eg. `tyConst `Bool`).
+  to build `Type` (eg. `tyConst @Bool`).
 * `TypeFamilies` for type-level programming.
 * `TypeInType` (introduced in GHC 8.0.1)
   for `Type` to also bind a kind equality for the type `t` it encodes.
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,7 @@
+resolver: lts-10.5
+packages:
+- '.'
+- location: '../symantic-grammar'
+  extra-dep: true
+- location: '../symantic-document'
+  extra-dep: true
diff --git a/symantic.cabal b/symantic.cabal
--- a/symantic.cabal
+++ b/symantic.cabal
@@ -1,52 +1,35 @@
-author: Julien Moutinho <julm+symantic@autogeree.net>
-bug-reports: Julien Moutinho <julm+symantic@autogeree.net>
-build-type: Simple
-cabal-version: >= 1.24
-category: Language
+name: symantic
+-- PVP:  +-+------- breaking API changes
+--       | | +----- non-breaking API additions
+--       | | | +--- code changes with no API change
+version: 6.3.1.20180213
+synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
 description: This is an experimental library for composing, parsing,
              typing, compiling, transforming and interpreting
              a custom DSL (Domain-Specific Language)
              expressing a subset of GHC's Haskell type system.
 extra-doc-files: README.md
-extra-source-files:
-extra-tmp-files:
--- homepage: 
+category: Language
 license: GPL-3
 license-file: COPYING
-maintainer: Julien Moutinho <julm+symantic@autogeree.net>
-name: symantic
 stability: experimental
-synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
-tested-with: GHC==8.0.2
--- PVP:  +-+------- breaking API changes
---       | | +----- non-breaking API additions
---       | | | +--- code changes with no API change
-version: 6.3.0.20170807
+author:      Julien Moutinho <julm+symantic@autogeree.net>
+maintainer:  Julien Moutinho <julm+symantic@autogeree.net>
+bug-reports: Julien Moutinho <julm+symantic@autogeree.net>
+-- homepage:
 
+build-type: Simple
+cabal-version: >= 1.24
+tested-with: GHC==8.2.2
+extra-source-files:
+  stack.yaml
+extra-tmp-files:
+
 Source-Repository head
   location: git://git.autogeree.net/symantic
   type:     git
 
 Library
-  default-extensions:
-    DataKinds
-    DefaultSignatures
-    FlexibleContexts
-    FlexibleInstances
-    LambdaCase
-    MultiParamTypeClasses
-    NamedFieldPuns
-    OverloadedStrings
-    Rank2Types
-    ScopedTypeVariables
-    StandaloneDeriving
-    TupleSections
-    TypeApplications
-    TypeFamilies
-    TypeOperators
-  ghc-options: -Wall
-               -fno-warn-tabs
-  default-language: Haskell2010
   exposed-modules:
     Language.Symantic
     Language.Symantic.Compiling
@@ -74,11 +57,34 @@
     Language.Symantic.Typing.Type
     Language.Symantic.Typing.Unify
     Language.Symantic.Typing.Variable
+  default-language: Haskell2010
+  default-extensions:
+    DataKinds
+    DefaultSignatures
+    FlexibleContexts
+    FlexibleInstances
+    LambdaCase
+    MultiParamTypeClasses
+    NamedFieldPuns
+    OverloadedStrings
+    Rank2Types
+    ScopedTypeVariables
+    StandaloneDeriving
+    TupleSections
+    TypeApplications
+    TypeFamilies
+    TypeOperators
+  ghc-options:
+    -Wall
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -fno-warn-tabs
+    -fhide-source-paths
   build-depends:
-    base >= 4.6 && < 5
-    , containers
-    , mono-traversable
-    , symantic-grammar
+      symantic-grammar
     , symantic-document
-    , transformers
-    , text
+    , base             >= 4.6 && < 5
+    , containers       >= 0.5
+    , mono-traversable >= 1.0
+    , transformers     >= 0.5
+    , text             >= 1.2