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
@@ -119,15 +119,15 @@
 deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g)
 instance
  ( Gram_Source src EBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Term_Type src EBNF
 instance
  ( Gram_Source src RuleEBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Term_Type src RuleEBNF
 
 -- ** Type 'Error_Term_Gram'
@@ -316,16 +316,16 @@
 instance
  ( Gram_Term_Atoms src ss EBNF
  , Gram_Source src EBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Term src ss EBNF
 instance
  ( Gram_Term_Atoms src ss RuleEBNF
  , Gram_Source src RuleEBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Term src ss RuleEBNF
 
 -- ** Class 'Gram_Term_Atoms'
diff --git a/Language/Symantic/Compiling/Read.hs b/Language/Symantic/Compiling/Read.hs
--- a/Language/Symantic/Compiling/Read.hs
+++ b/Language/Symantic/Compiling/Read.hs
@@ -19,15 +19,13 @@
  SourceInj (KindK src) src =>
  SourceInj (AST_Type src) src =>
  Constable (->) =>
- Imports NameTy ->
- ModulesTy src ->
  CtxTy src ts ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss ts)
 
 -- | Read a 'TermVT' from and 'AST_Term'.
 readTerm :: forall src ss ts. ReadTerm src ss ts
-readTerm impsTy modsTy ctxTy ast = do
+readTerm ctxTy ast = do
 	ts <- go ctxTy `traverse` ast
 	errorInj `left` betaTerms ts
 	where
@@ -41,12 +39,12 @@
 	go ts  (Token_Term_Var _src name) = teVar name ts
 	go _ts (Token_Term_App _src)      = Right $ TermVT teApp
 	go ts  (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
-		TypeVT ty_arg <- errorInj `left` readType impsTy modsTy ast_ty_arg
+		TypeVT ty_arg <- errorInj `left` readType ast_ty_arg
 		when_EqKind (kindInj @K.Type) (kindOf ty_arg) $ \Refl ->
 			case lenVars ty_arg of
 			 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
 			 LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
-				TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name_arg ta ts) ast_body
+				TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name_arg ta ts) ast_body
 				let (qa', qr') = appendVars qa qr
 				let (ta', tr') = appendVars ta tr
 				Right $
@@ -65,11 +63,11 @@
 						Term (qa' # qr') (ta' ~> tr') $
 						TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
 	go ts (Token_Term_Let _src name ast_arg ast_body) = do
-		TermVT (Term qa ta (TeSym arg)) <- readTerm impsTy modsTy ts ast_arg
+		TermVT (Term qa ta (TeSym arg)) <- readTerm ts ast_arg
 		case lenVars ta of
 		 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
 		 LenZ -> do
-			TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body
+			TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name ta ts) ast_body
 			let (qa', qr') = appendVars qa qr
 			let tr' = allocVarsL (lenVars ta) tr
 			Right $
@@ -143,8 +141,6 @@
  SourceInj (AST_Type src) src =>
  Constable (->) =>
  f (NameTe, TermT src ss '[] '[]) ->
- Imports NameTy ->
- ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
 readTermWithCtx env =
@@ -167,8 +163,8 @@
  (NameTe, TermT src ss '[] '[]) ->
  (forall ts'. ReadTerm src ss ts') ->
  ReadTerm src ss ts
-readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe impsTy modsTy ctxTy ast = do
-	TermVT (Term q t (TeSym te)) <- readTe impsTy modsTy (CtxTyS n (qn #> tn) ctxTy) ast
+readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe ctxTy ast = do
+	TermVT (Term q t (TeSym te)) <- readTe (CtxTyS n (qn #> tn) ctxTy) ast
 	case proveConstraint qn of
 	 Nothing -> Left $ Error_Term_proofless $ TypeVT qn
 	 Just Dict ->
@@ -184,11 +180,9 @@
  SourceInj (KindK src) src =>
  SourceInj (AST_Type src) src =>
  Constable (->) =>
- Imports NameTy ->
- ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
-readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ
+readTermWithCtxClose readTe = readTe CtxTyZ
 
 -- * Type 'CtxTy'
 -- | /Typing context/
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
@@ -7,14 +7,14 @@
 
 import Control.Applicative (Applicative(..))
 import Data.List (foldl1')
-import Data.Proxy (Proxy(..))
+import Data.Map.Strict (Map)
+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.Text as Text
-import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import qualified Data.Text as Text
 
 import Language.Symantic.Grammar as G
 import Language.Symantic.Typing.Kind
@@ -29,15 +29,15 @@
 
 -- ** Type 'Token_Type'
 data Token_Type src
- =   Token_Type_Const (At src (Mod NameTy))
+ =   Token_Type_Const (TypeTLen src)
  |   Token_Type_Var   (At src NameVar)
  -- deriving (Eq, Show)
 instance Source src => Eq (Token_Type src) where
-	Token_Type_Const (At _ x) == Token_Type_Const (At _ y) = x == y
-	Token_Type_Var   (At _ x) == Token_Type_Var   (At _ y) = x == y
+	Token_Type_Const (TypeTLen x) == Token_Type_Const (TypeTLen y) = x LenZ == y LenZ
+	Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y
 	_ == _ = False
-instance Source src => Show (Token_Type src) where
-	showsPrec p (Token_Type_Const (At _ x)) =
+instance (Source src, Show (TypeT src '[])) => Show (Token_Type src) where
+	showsPrec p (Token_Type_Const x) =
 		showParen (p >= 10) $
 		showString "Token_Type_Const" .
 		showChar ' ' . showsPrec 10 x
@@ -60,6 +60,20 @@
 instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where
 	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
 
+typeTLen ::
+ forall c src.
+ Source src =>
+ Constable c =>
+ KindInjP (Ty_of_Type (K c)) =>
+ K c ~ Type_of_Ty (Ty_of_Type (K c)) =>
+ src ->
+ TypeTLen src
+typeTLen src =
+	TypeTLen $ \len -> TypeT $
+		TyConst src len $
+		constKiInj @(K c) @c $
+		kindInjP @(Ty_of_Type (K c)) noSource
+
 -- ** Class 'ModulesTyInj'
 -- | Derive a 'ModulesTy' from the given type-level list
 -- of 'Proxy'-fied /type constants/.
@@ -76,9 +90,7 @@
 	modulesTyInj =
 		Map.insert
 		 (nameTyOf $ Proxy @c)
-		 (TypeTLen $ \len -> TypeT $ TyConst noSource len $
-			constKiInj @(K c) @c $
-			kindInjP @(Ty_of_Type (K c)) noSource) $
+		 (typeTLen @c noSource) $
 		modulesTyInj @ts
 
 
@@ -187,16 +199,18 @@
  , Gram_Comment g
  , Gram_Op g
  , Gram_Type_Name g
- , NameTyOf (->)
- , NameTyOf []
- , NameTyOf (,)
+ , Gram_Error (Error_Type src) g
+ , Gram_State (Imports NameTy, ModulesTy src) g
+ , Constable (->)
+ , Constable []
+ , Constable (,)
  ) => Gram_Type src g where
 	g_type :: CF g (AST_Type src)
 	g_type = rule "type" $ g_type_fun
 	g_type_fun :: CF g (AST_Type src)
 	g_type_fun = rule "type_fun" $
 		infixrG g_type_list (source $ op <$ symbol "->")
-		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(->))
+		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" $
@@ -206,11 +220,11 @@
 		where
 		mk Nothing  src = tok src
 		mk (Just a) src = BinTree2 (tok src) a
-		tok src = BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @[]
+		tok = BinTree0 . Token_Type_Const . typeTLen @[]
 	g_type_tuple2 :: CF g (AST_Type src)
 	g_type_tuple2 = rule "type_tuple2" $
 		try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
-		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(,))
+		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" $
 		foldl1' BinTree2 <$> some (g_type_atom)
@@ -219,48 +233,55 @@
 		try (parens g_type) <+>
 		g_type_name_const <+>
 		g_type_name_var
-		-- <+> g_type_symbol
 	g_type_name_const :: CF g (AST_Type src)
 	g_type_name_const = rule "type_name_const" $
-		lexeme $ source $
-		(\n src -> BinTree0 $ Token_Type_Const $ At src n)
+		lexeme $ catch $ source $ getBefore $
+		(\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
 		 <$> g_ModNameTy
-		 -- <$> unicat (Unicat Char.UppercaseLetter)
-		 -- <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
 	g_type_name_var :: CF g (AST_Type src)
 	g_type_name_var = rule "type_name_var" $
 		lexeme $ source $
 		(\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
 		 <$> unicat (Unicat Char.LowercaseLetter)
 		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
-	{-
-	g_type_symbol :: CF g (AST_Type src)
-	g_type_symbol = rule "type_symbol" $
-		source $ (mk <$>) $
-		parens $ many $ cfOf $ choice g_ok `but` choice g_ko
-		where
-		mk s src = BinTree0 $ Token_Type_Const $ At src $ Mod [] $ fromString $ "(" ++ s ++ ")"
-		g_ok = unicat <$>
-		 [ Unicat_Symbol
-		 , Unicat_Punctuation
-		 , Unicat_Mark
-		 ]
-		g_ko = char <$> ['(', ')', '`']
-	-}
 
 deriving instance Gram_Type src g => Gram_Type src (CF g)
 instance
  ( Gram_Source src EBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Type src EBNF
 instance
  ( Gram_Source src RuleEBNF
- , NameTyOf (->)
- , NameTyOf (,)
- , NameTyOf []
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Type src RuleEBNF
+
+-- | Lookup a 'TyConst' or 'Type' synonym
+-- associated with given 'NameTy' in given 'ModulesTy',
+-- building it for a @vs@ of given 'Len'.
+readTyName ::
+ Source src =>
+ Imports NameTy ->
+ ModulesTy src -> src -> Mod NameTy ->
+ Either (Error_Type src) (TypeTLen src)
+readTyName is ms src name@(m `Mod` n) =
+	let m' = fromMaybe m $ lookupImports FixyInfix name is in
+	case Map.lookup (m' `Mod` n) ms of
+	 Just t -> Right t
+	 Nothing -> Left $ Error_Type_Constant_unknown $ At src name
+
+-- * Type 'Error_Type'
+data Error_Type src
+ =   Error_Type_Constant_unknown (At src (Mod NameTy))
+ |   Error_Type_Con_Kind         (Con_Kind src)
+ deriving (Eq, Show)
+instance ErrorInj (Error_Type src) (Error_Type src) where
+	errorInj = id
+instance ErrorInj (Con_Kind src) (Error_Type src) where
+	errorInj = Error_Type_Con_Kind
 
 -- | List of the rules of 'Gram_Type'.
 gram_type :: Gram_Type () g => [CF g (AST_Type ())]
diff --git a/Language/Symantic/Typing/Read.hs b/Language/Symantic/Typing/Read.hs
--- a/Language/Symantic/Typing/Read.hs
+++ b/Language/Symantic/Typing/Read.hs
@@ -2,30 +2,22 @@
 {-# LANGUAGE PolyKinds #-}
 module Language.Symantic.Typing.Read where
 
-import Data.Maybe (fromMaybe)
-import Data.Typeable
-import qualified Data.Map.Strict as Map
-
 import Language.Symantic.Grammar
-import Language.Symantic.Typing.List
 import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Type
 import Language.Symantic.Typing.Show ()
 import Language.Symantic.Typing.Grammar
 import Language.Symantic.Typing.Variable
-import Language.Symantic.Typing.Module
 
 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
 readType ::
  SourceInj (KindK src) src =>
  SourceInj (TypeVT src) src =>
  SourceInj (AST_Type src) src =>
- Imports NameTy ->
- ModulesTy src ->
  AST_Type src ->
  Either (Error_Type src) (TypeVT src)
-readType is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do
-	TypeT ty <- readTyVars is ms vs ast
+readType ast | EVars vs <- readVars (EVars VarsZ) ast = do
+	TypeT ty <- readTyVars vs ast
 	Right $ TypeVT ty
 
 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
@@ -34,38 +26,23 @@
  SourceInj (KindK src) src =>
  SourceInj (TypeVT src) src =>
  SourceInj (AST_Type src) src =>
- Imports NameTy ->
- ModulesTy src ->
  Vars src vs ->
  AST_Type src ->
  Either (Error_Type src) (TypeT src vs)
-readTyVars is ms vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
-	readTyName is ms (sourceInj ast) (lenVars vs) name
-readTyVars _is _ms vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
+readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =
+	Right $ t (lenVars vs)
+	-- readTyName is ms (sourceInj ast) (lenVars vs) name
+readTyVars vs (BinTree0 (Token_Type_Var (At src name))) =
 	case lookupVars name vs of
-	 Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v
+	 Just (EVar v) -> Right $ TypeT $ TyVar src name v
 	 Nothing -> error "[BUG] readTyVars: lookupVars failed"
-readTyVars is ms vs ast@(ast_x `BinTree2` ast_y) = do
-	TypeT ty_x <- readTyVars is ms vs ast_x
-	TypeT ty_y <- readTyVars is ms vs ast_y
+readTyVars vs ast@(ast_x `BinTree2` ast_y) = do
+	TypeT ty_x <- readTyVars vs ast_x
+	TypeT ty_y <- readTyVars vs ast_y
 	when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
 		when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
 			Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
 
--- | Lookup a 'TyConst' or 'Type' synonym
--- associated with given 'NameTy' in given 'ModulesTy',
--- building it for a @vs@ of given 'Len'.
-readTyName ::
- Source src =>
- Imports NameTy ->
- ModulesTy src -> src -> Len vs -> Mod NameTy ->
- Either (Error_Type src) (TypeT src vs)
-readTyName is ms src len name@(m `Mod` n) =
-	let m' = fromMaybe m $ lookupImports FixyInfix name is in
-	case Map.lookup (m' `Mod` n) ms of
-	 Just (TypeTLen t) -> Right $ t len
-	 Nothing -> Left $ Error_Type_Constant_unknown $ At src name
-
 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
 readVars :: Source src => EVars src -> AST_Type src -> EVars src
 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
@@ -78,13 +55,3 @@
 readVars evs BinTree0{} = evs
 readVars evs (BinTree2 x y) =
 	readVars (readVars evs x) y
-
--- * Type 'Error_Type'
-data Error_Type src
- =   Error_Type_Constant_unknown (At src (Mod NameTy))
- |   Error_Type_Con_Kind         (Con_Kind src)
- deriving (Eq, Show)
-instance ErrorInj (Error_Type src) (Error_Type src) where
-	errorInj = id
-instance ErrorInj (Con_Kind src) (Error_Type src) where
-	errorInj = Error_Type_Con_Kind
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,10 +1,10 @@
-{-# language ConstraintKinds #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
+{-# language ConstraintKinds #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Typing.Type
  ( module Language.Symantic.Typing.Type
diff --git a/symantic.cabal b/symantic.cabal
--- a/symantic.cabal
+++ b/symantic.cabal
@@ -20,7 +20,7 @@
 -- PVP:  +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 6.2.0.20170702
+version: 6.3.0.20170703
 
 Source-Repository head
   location: git://git.autogeree.net/symantic
@@ -76,7 +76,6 @@
   build-depends:
     base >= 4.6 && < 5
     , containers
-    , ghc-prim
     , mono-traversable
     , symantic-grammar
     , symantic-document