diff --git a/Language/Symantic.hs b/Language/Symantic.hs
--- a/Language/Symantic.hs
+++ b/Language/Symantic.hs
@@ -5,7 +5,8 @@
  , module Language.Symantic.Transforming
  -- * Re-exports for convenience.
  , module Language.Symantic.Grammar.Fixity
- , module Language.Symantic.Grammar.Meta
+ , module Language.Symantic.Grammar.Source
+ , module Language.Symantic.Grammar.Error
  ) where
 
 import Language.Symantic.Typing
@@ -14,4 +15,5 @@
 import Language.Symantic.Transforming
 
 import Language.Symantic.Grammar.Fixity
-import Language.Symantic.Grammar.Meta
+import Language.Symantic.Grammar.Source
+import Language.Symantic.Grammar.Error
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
@@ -12,7 +12,7 @@
 -- applying embedded 'TeSym's, or return an error.
 betaTerm ::
  forall src ss es vs fun arg.
- Inj_Source (TypeVT src) src =>
+ SourceInj (TypeVT src) src =>
  Constable (->) =>
  Term src ss es vs (fun::K.Type) ->
  Term src ss es vs (arg::K.Type) ->
@@ -39,7 +39,7 @@
 
 -- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.
 betaTerms ::
- Inj_Source (TypeVT src) src =>
+ SourceInj (TypeVT src) src =>
  Constable (->) =>
  BinTree (TermVT src ss es) ->
  Either (Error_Beta src) (TermVT src ss es)
@@ -74,7 +74,7 @@
      -- with the 'Type' of the argument.
  deriving (Eq, Show)
 
-instance Inj_Error (Error_Beta src) (Error_Beta src) where
-	inj_Error = id
-instance Inj_Error (Error_Unify src) (Error_Beta src) where
-	inj_Error = Error_Beta_Unify
+instance ErrorInj (Error_Beta src) (Error_Beta src) where
+	errorInj = id
+instance ErrorInj (Error_Unify src) (Error_Beta src) where
+	errorInj = Error_Beta_Unify
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
@@ -8,19 +8,18 @@
 
 import Control.Arrow (left)
 import Control.Monad (void)
-import Data.Proxy (Proxy(..))
 import Data.Semigroup (Semigroup(..))
+import Data.Map.Strict (Map)
 import Prelude hiding (mod, not, any)
-import qualified Data.Char as Char
 import qualified Data.Function as Fun
 import qualified Data.Map.Strict as Map
 import qualified Data.Text as Text
 
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
 import Language.Symantic.Typing
 import Language.Symantic.Compiling.Module
 
--- * Class 'Gram_Name'
+-- * Class 'Gram_Term_Name'
 class
  ( Gram_Terminal g
  , Gram_Rule g
@@ -32,74 +31,56 @@
  , Gram_CF g
  , Gram_Comment g
  , Gram_Op g
- ) => Gram_Name g where
-	g_mod_path :: CF g PathMod
-	g_mod_path = rule "mod_path" $
-		infixrG
-		 (pure <$> g_mod_name)
-		 (op <$ char '.')
-		where op = (<>)
-	g_mod_name :: CF g NameMod
-	g_mod_name = rule "mod_name" $
-		(NameMod . Text.pack <$>) $
-		(identG `minus`) $
-		Fun.const
-		 <$> g_term_keywords
-		 <*. (any `but` g_term_idname_tail)
-		where
-		identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
-		headG  = unicat $ Unicat Char.UppercaseLetter
-	
-	g_term_mod_name :: CF g (Mod NameTe)
-	g_term_mod_name = rule "term_mod_name" $
+ , Gram_Mod g
+ ) => Gram_Term_Name g where
+	g_ModNameTe :: CF g (Mod NameTe)
+	g_ModNameTe = rule "ModNameTe" $
 		lexeme $
-			g_term_mod_idname <+>
-			parens g_term_mod_opname
-	g_term_name :: CF g NameTe
-	g_term_name = rule "term_name" $
+			g_ModNameTeId <+>
+			parens g_ModNameTeOp
+	g_NameTe :: CF g NameTe
+	g_NameTe = rule "NameTe" $
 		lexeme $
-			g_term_idname <+>
-			parens g_term_opname
+			g_NameTeId <+>
+			parens g_NameTeOp
 	
-	g_term_mod_idname :: CF g (Mod NameTe)
-	g_term_mod_idname = rule "term_mod_idname" $
+	g_ModNameTeId :: CF g (Mod NameTe)
+	g_ModNameTeId = rule "ModNameTeId" $
 		Mod
-		 <$> option [] (try $ g_mod_path <* char '.')
-		 <*> g_term_idname
-	g_term_idname :: CF g NameTe
-	g_term_idname = rule "term_idname" $
+		 <$> option [] (try $ g_PathMod <* char '.')
+		 <*> g_NameTeId
+	g_NameTeId :: CF g NameTe
+	g_NameTeId = rule "NameTeId" $
 		(NameTe . Text.pack <$>) $
 		(identG `minus`) $
 		Fun.const
-		 <$> g_term_keywords
-		 <*. (any `but` g_term_idname_tail)
+		 <$> g_NameTeKey
+		 <*. (any `but` g_NameTeIdTail)
 		where
-		identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
+		identG = (:) <$> headG <*> many (cfOf g_NameTeIdTail)
 		headG  = unicat $ Unicat_Letter
-	g_term_idname_tail :: Terminal g Char
-	g_term_idname_tail = rule "term_idname_tail" $
+	g_NameTeIdTail :: Terminal g Char
+	g_NameTeIdTail = rule "NameTeIdTail" $
 		unicat Unicat_Letter <+>
 		unicat Unicat_Number
-	g_term_keywords :: Reg rl g String
-	g_term_keywords = rule "term_keywords" $
+	g_NameTeKey :: Reg rl g String
+	g_NameTeKey = rule "NameTeKey" $
 		choice $ string <$> ["in", "let"]
 	
-	g_term_mod_opname :: CF g (Mod NameTe)
-	g_term_mod_opname = rule "term_mod_opname" $
+	g_ModNameTeOp :: CF g (Mod NameTe)
+	g_ModNameTeOp = rule "ModNameTeOp" $
 		Mod
-		 <$> option [] (try $ g_mod_path <* char '.')
-		 <*> g_term_opname
-	g_term_opname :: CF g NameTe
-	g_term_opname = rule "term_opname" $
+		 <$> option [] (try $ g_PathMod <* char '.')
+		 <*> g_NameTeOp
+	g_NameTeOp :: CF g NameTe
+	g_NameTeOp = rule "NameTeOp" $
 		(NameTe . Text.pack <$>) $
-		(symG `minus`) $
+		(some (cfOf g_NameTeOpOk) `minus`) $
 		Fun.const
-		 <$> g_term_keysyms
-		 <*. (any `but` g_term_opname_ok)
-		where
-		symG = some $ cf_of_Terminal g_term_opname_ok
-	g_term_opname_ok :: Terminal g Char
-	g_term_opname_ok = rule "term_opname_ok" $
+		 <$> g_NameTeKeySym
+		 <*. (any `but` g_NameTeOpOk)
+	g_NameTeOpOk :: Terminal g Char
+	g_NameTeOpOk = rule "NameTeOpOk" $
 		choice (unicat <$>
 		 [ Unicat_Symbol
 		 , Unicat_Punctuation
@@ -107,13 +88,13 @@
 		 ]) `but` koG
 		where
 		koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])
-	g_term_keysyms :: Reg rl g String
-	g_term_keysyms = rule "term_keysyms" $
+	g_NameTeKeySym :: Reg rl g String
+	g_NameTeKeySym = rule "NameTeKeySym" $
 		choice $ string <$> ["\\", "->", "=", "@"]
 
-deriving instance Gram_Name g => Gram_Name (CF g)
-instance Gram_Name EBNF
-instance Gram_Name RuleEBNF
+deriving instance Gram_Term_Name g => Gram_Term_Name (CF g)
+instance Gram_Term_Name EBNF
+instance Gram_Term_Name RuleEBNF
 
 -- * Class 'Gram_Term_Type'
 class
@@ -124,20 +105,30 @@
  , Gram_App g
  , Gram_CF g
  , Gram_Comment g
- , Gram_Name g
+ , Gram_Term_Name g
  , 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" $
 		parens $ (,)
-		 <$> g_term_name
+		 <$> g_NameTe
 		 <*  (symbol "::" <+> symbol ":")
 		 -- NOTE: "::" is Haskell compatibility and ":" is another common notation.
 		 <*> g_type
 
 deriving instance Gram_Term_Type src g => Gram_Term_Type src (CF g)
-instance Gram_Source src EBNF => Gram_Term_Type src EBNF
-instance Gram_Source src RuleEBNF => Gram_Term_Type src RuleEBNF
+instance
+ ( Gram_Source src EBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
+ ) => Gram_Term_Type src EBNF
+instance
+ ( Gram_Source src RuleEBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
+ ) => Gram_Term_Type src RuleEBNF
 
 -- ** Type 'Error_Term_Gram'
 data Error_Term_Gram
@@ -162,10 +153,10 @@
  , Gram_CF g
  , Gram_Comment g
  , Gram_Type src g
- , Gram_Name g
+ , Gram_Term_Name g
  , Gram_Term_Type src g
  , Gram_Term_Atoms src ss g
- , Gram_State (Imports, Modules src ss) g
+ , 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" $
@@ -176,7 +167,7 @@
 		 ]
 	g_term_operators :: CF g  (AST_Term src ss)
 	g_term_operators = rule "term_operators" $
-		g_catch $
+		G.catch $
 		left Error_Term_Gram_Fixity <$>
 		g_ops
 		where
@@ -185,53 +176,53 @@
 		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_get_after $ op_prefix  <$> g_prefix_op
-		g_infix   = g_catch $ g_source $ g_get_after $ op_infix   <$> g_infix_op
-		g_postfix = g_catch $ g_source $ g_get_after $ op_postfix <$> g_postfix_op
+		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, Modules src ss)
+		 -> (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 FixitySing_Infix imps name mods
+				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, Modules src ss)
+		 -> (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 FixitySing_Prefix imps name mods
+				lookupDefTerm FixyPrefix imps name mods
 			Right $ (token_fixity t,) $ \a ->
 				BinTree0 (token_term t src) `BinTree2` a
 		op_postfix name (imps, mods) src = do
 			t <- Error_Term_Gram_Module `left`
-				lookupDefTerm FixitySing_Postfix imps name mods
+				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" $
 			lexeme $
-				g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote)
-				g_term_mod_opname
+				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" $
 			lexeme $
-				between g_backquote g_backquote g_term_mod_idname <+>
-				try (Fun.const <$> g_term_mod_opname <*> (string " " <+> string "\n")) <+>
+				between g_backquote g_backquote g_ModNameTeId <+>
+				try (Fun.const <$> g_ModNameTeOp <*> (string " " <+> string "\n")) <+>
 				pure (Mod [] " ")
 		g_prefix_op :: CF g (Mod NameTe)
 		g_prefix_op = rule "term_op_prefix" $
 			lexeme $
-				g_term_mod_idname <* g_backquote <+>
-				g_term_mod_opname
+				g_ModNameTeId <* g_backquote <+>
+				g_ModNameTeOp
 		g_backquote :: Gram_Terminal g' => g' Char
 		g_backquote = char '`'
 	
@@ -239,28 +230,28 @@
 	g_term_atom = rule "term_atom" $
 		choice $
 		 {-(try (
-			g_source $
+			G.source $
 			(\typ src -> BinTree0 $ inj_EToken src $ Token_Term_Type typ)
 			 <$ char '@' <*> g_type) :) $
 		 -}
 		 (try <$> g_term_atomsR @_ @_ @ss) <>
 		 [ try $
-			g_catch $ g_source $ g_get_after $
+			G.catch $ G.source $ G.getAfter $
 			(\m (imps, mods) src ->
-				case lookupDefTerm FixitySing_Infix imps m mods of
+				case lookupDefTerm FixyInfix imps m mods of
 				 Right t -> Right $ BinTree0 $ token_term t src
 				 Left err ->
 					case m of
 					 [] `Mod` n -> Right $ BinTree0 $ Token_Term_Var src n
 					 _ -> Left $ Error_Term_Gram_Module err
-			 ) <$> g_term_mod_name
+			 ) <$> g_ModNameTe
 		 , g_term_group
 		 ]
 	g_term_group :: CF g (AST_Term src ss)
 	g_term_group = rule "term_group" $ parens g_term
 	g_term_abst :: CF g (AST_Term src ss)
 	g_term_abst = rule "term_abst" $
-		g_source $
+		G.source $
 		((\(xs, te) src ->
 			foldr (\(x, ty_x) ->
 				BinTree0 . Token_Term_Abst src x ty_x) te xs) <$>) $
@@ -273,37 +264,45 @@
 	 -> CF g ([(NameTe, AST_Type src)], AST_Term src ss)
 	-- g_term_abst_args_body args body = (,) <$> args <*> body
 	g_term_abst_args_body cf_args cf_body =
-		g_state_before $
-		(\a b (imps::Imports, mods::Modules src ss) -> ((imps, mods), (a, b)))
-		 <$> g_state_after ((<$> cf_args) $ \args (imps::Imports, Modules mods) ->
-			((imps, Modules $ Map.alter (setArgs args) [] mods), args))
+		G.stateBefore $
+		(\a b (imps::Imports NameTe, mods::Modules src ss) -> ((imps, mods), (a, b)))
+		 <$> G.stateAfter ((<$> cf_args) $ \args (imps::Imports NameTe, mods) ->
+			((setArgsImps args imps, setArgsMods args mods), args))
 		 <*> cf_body
 		where
-		setArgs args = \case
-		 Nothing -> Just $ moduleEmpty {module_infix = insArg mempty args}
-		 Just mod -> Just $ mod
-			 { module_prefix  = delArg (module_prefix  mod) args
-			 , module_infix   = insArg (module_infix   mod) args
-			 , module_postfix = delArg (module_postfix mod) args
+		setArgsImps args (Imports imps) = Imports $ Map.alter (alterArgsImps args) [] imps
+		alterArgsImps args = \case
+		 Nothing -> Just mempty
+		 Just m -> Just $ mapMapFixity (delArgImp args) m
+		delArgImp :: [(NameTe, _a)] -> Map NameTe PathMod -> Map NameTe PathMod
+		delArgImp = flip $ foldr $ \(n, _) -> Map.delete n
+		
+		setArgsMods args (Modules mods) = Modules $ Map.alter (alterArgsMods args) [] mods
+		alterArgsMods args = \case
+		 Nothing -> Just moduleEmpty{byInfix = mempty `insArgMod` args}
+		 Just m -> Just m
+			 { byPrefix  = byPrefix  m `delArgMod` args
+			 , byInfix   = byInfix   m `insArgMod` args
+			 , byPostfix = byPostfix m `delArgMod` args
 			 }
-		delArg :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix
-		delArg = foldr $ \(n, _) -> Map.delete n
-		insArg :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix
-		insArg = foldr $ \(n, _) ->
+		delArgMod :: ModuleFixy src ss Unifix -> [(NameTe, _a)] -> ModuleFixy src ss Unifix
+		delArgMod = foldr $ \(n, _) -> Map.delete n
+		insArgMod :: ModuleFixy src ss Infix -> [(NameTe, _a)] -> ModuleFixy src ss Infix
+		insArgMod = foldr $ \(n, _) ->
 			Map.insert n Tokenizer
 			 { token_term   = (`Token_Term_Var` n)
 			 , token_fixity = infixN5
 			 }
 	g_term_let :: CF g  (AST_Term src ss)
 	g_term_let = rule "term_let" $
-		g_source $
+		G.source $
 		(\name args bound body src ->
 			BinTree0 $
 			Token_Term_Let src name
 			 (foldr (\(x, ty_x) ->
 				BinTree0 . Token_Term_Abst src x ty_x) bound args) body)
 		 <$  symbol "let"
-		 <*> g_term_name
+		 <*> g_NameTe
 		 <*> many g_term_abst_decl
 		 <*  symbol "="
 		 <*> g_term
@@ -317,10 +316,16 @@
 instance
  ( Gram_Term_Atoms src ss EBNF
  , Gram_Source src EBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
  ) => Gram_Term src ss EBNF
 instance
  ( Gram_Term_Atoms src ss RuleEBNF
  , Gram_Source src RuleEBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
  ) => Gram_Term src ss RuleEBNF
 
 -- ** Class 'Gram_Term_Atoms'
@@ -356,15 +361,15 @@
  , voiD g_term_abst
  , void (g_term_abst_decl::CF g (NameTe, AST_Type ()))
  , voiD g_term_let
- , void g_term_mod_name
- , void g_term_name
- , void g_term_idname
- , void $ cf_of_Terminal g_term_idname_tail
- , void $ cf_of_Reg g_term_keywords
- , void g_term_mod_opname
- , void g_term_opname
- , void $ cf_of_Terminal g_term_opname_ok
- , void $ cf_of_Reg g_term_keysyms
+ , void g_ModNameTe
+ , void g_NameTe
+ , void g_NameTeId
+ , void $ G.cfOf g_NameTeIdTail
+ , void $ G.cfOf g_NameTeKey
+ , void g_ModNameTeOp
+ , void g_NameTeOp
+ , void $ G.cfOf g_NameTeOpOk
+ , void $ G.cfOf g_NameTeKeySym
  ] 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
@@ -1,6 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -10,43 +9,33 @@
 
 import Data.Bool (not)
 import Data.Map.Strict (Map)
+import Data.Maybe (fromMaybe)
 import Data.Semigroup (Semigroup(..))
 import Data.Set (Set)
 import Data.String (IsString(..))
-import Data.Text (Text)
 import Prelude hiding (mod, not, any)
-import qualified Data.Kind as K
 import qualified Data.Map.Strict as Map
 
 import Language.Symantic.Grammar
 import Language.Symantic.Typing
 import Language.Symantic.Compiling.Term
 
--- * Type 'Mod'
-data Mod a = Mod PathMod a
- deriving (Eq, Functor, Ord, Show)
-
--- ** Type 'PathMod'
-type PathMod = [NameMod]
-
--- ** Type 'NameMod'
-newtype NameMod = NameMod Text
- deriving (Eq, Ord, Show)
-instance IsString NameMod where
-	fromString = NameMod . fromString
-
 -- * Class 'ModuleFor'
 class ModuleFor src ss s where
 	moduleFor :: (PathMod, Module src ss)
 	moduleFor = ([], moduleEmpty)
 
--- * Type 'Imports'
-newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))
- deriving (Eq, Show)
-type FilterImports = Maybe (Set NameTe)
-
-importQualifiedAs :: PathMod -> Modules src ss -> Imports
-importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]
+importModules :: PathMod -> Modules src ss -> Imports NameTe
+importModules as (Modules mods) =
+	Imports $ Map.singleton as $
+	Map.foldrWithKey
+	 (\pm (ByFixity mp mi mq) acc ->
+		acc <> ByFixity
+		 { byPrefix  = pm <$ mp
+		 , byInfix   = pm <$ mi
+		 , byPostfix = pm <$ mq
+		 }
+	 ) mempty mods
 
 -- * Type 'Modules'
 newtype Modules src ss
@@ -71,9 +60,9 @@
 			let errs =
 				Map.filter (not . null) $
 				(<$> xy) $ \(a, b) ->
-					inter a b module_prefix <>
-					inter a b module_infix <>
-					inter a b module_postfix in
+					inter a b byPrefix <>
+					inter a b byInfix <>
+					inter a b byPostfix in
 			case errs of
 			 e | null e -> Nothing
 			 e -> Just $ Error_Module_colliding_Term e
@@ -89,74 +78,61 @@
  =   Error_Module_colliding_Term (Map PathMod (Set NameTe))
  |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)
  |   Error_Module_missing PathMod
- |   Error_Module_missing_Term (Mod NameTe)
+ |   Error_Module_missing_Term (Mod NameTe) -- FixyA
  deriving (Eq, Show)
 
 -- ** Type 'Module'
-data Module src ss
- =   Module
- {   module_prefix  :: ModuleFixy src ss Unifix
- ,   module_infix   :: ModuleFixy src ss Infix
- ,   module_postfix :: ModuleFixy src ss Unifix
- } deriving (Eq, Show)
-
-module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy
-module_fixity = \case
-	 FixitySing_Prefix  -> module_prefix
-	 FixitySing_Infix   -> module_infix
-	 FixitySing_Postfix -> module_postfix
+type Module src ss = ByFixity (ModuleFixy src ss Unifix)
+                              (ModuleFixy src ss Infix)
+                              (ModuleFixy src ss Unifix)
 
 moduleEmpty :: Module src ss
-moduleEmpty = Module
- { module_prefix  = mempty
- , module_infix   = mempty
- , module_postfix = mempty
+moduleEmpty = ByFixity
+ { byPrefix  = mempty
+ , byInfix   = mempty
+ , byPostfix = mempty
  }
 
 moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
 moduleWhere mod lst =
-	(mod,) Module
-	 { module_infix = mk $ \(n `WithFixity` fixy := t) ->
+	(mod,) ByFixity
+	 { byInfix = mk $ \(n `WithFixity` fixy := t) ->
 		case fixy of
 		 Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
 		 _ -> []
-	 , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
+	 , byPrefix = mk $ \(n `WithFixity` fixy := t) ->
 		case fixy of
 		 Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
 		 _ -> []
-	 , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
+	 , byPostfix = mk $ \(n `WithFixity` fixy := t) ->
 		case fixy of
 		 Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]
 		 _ -> []
 	 }
 	where
 	mk ::
-	 (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->
-	 Map NameTe (Tokenizer fixy src ss)
+	 (DefTerm src ss -> [(NameTe, Tokenizer src ss fixy)]) ->
+	 Map NameTe (Tokenizer src ss fixy)
 	mk = Map.fromList . (`foldMap` lst)
 
 -- *** Type 'ModuleFixy'
-type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)
-
-instance Semigroup (Module src ss) where
-	x <> y =
-		Module
-		 { module_prefix  = module_prefix  x <> module_prefix  y
-		 , module_infix   = module_infix   x <> module_infix   y
-		 , module_postfix = module_postfix x <> module_postfix y
-		 }
+type ModuleFixy src ss fixy = Map NameTe (Tokenizer src ss fixy)
 
 -- ** Type 'Tokenizer'
-data Tokenizer fixy src ss
+data Tokenizer src ss fixy
  =   Tokenizer
  {   token_fixity :: fixy
  ,   token_term   :: src -> Token_Term src ss
  }
-instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where
+instance (Source src, Eq fixy) => Eq (Tokenizer src ss fixy) where
 	Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)
-instance Source src => Show (Tokenizer fixy src ss) where
+instance Source src => Show (Tokenizer src ss fixy) where
 	show (Tokenizer _fx x) = show (x noSource)
 
+-- ** Type 'AST_Term'
+-- | /Abstract Syntax Tree/ of 'Token_Term'.
+type AST_Term src ss = BinTree (Token_Term src ss)
+
 -- ** Type 'Token_Term'
 data Token_Term src ss
  =   Token_Term      (TermAVT src ss)
@@ -202,59 +178,34 @@
 	showsPrec _p (Token_Term_App _) = showString "Token_Term_App"
 
 -- ** Type 'NameTe'
-newtype NameTe = NameTe Text
+newtype NameTe = NameTe Name
  deriving (Eq, Ord, Show)
 instance IsString NameTe where
 	fromString = NameTe . fromString
-
--- * Type 'CtxTy'
--- | /Typing context/
--- accumulating at each /lambda abstraction/
--- the 'Type' of the introduced variable.
--- It is built top-down from the closest
--- including /lambda abstraction/ to the farest.
-data CtxTy src (ts::[K.Type]) where
-	CtxTyZ :: CtxTy src '[]
-	CtxTyS :: NameTe
-	       -> Type  src '[] t
-	       -> CtxTy src ts
-	       -> CtxTy src (t ': ts)
-infixr 5 `CtxTyS`
-
-appendCtxTy
- :: CtxTy src ts0
- -> CtxTy src ts1
- -> CtxTy src (ts0 ++ ts1)
-appendCtxTy CtxTyZ c          = c
-appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
-
-
-
--- ** Type 'AST_Term'
--- | /Abstract Syntax Tree/ of 'Token_Term'.
-type AST_Term src ss = BinTree (Token_Term src ss)
+instance NameOf NameTe where
+	nameOf (NameTe n) = n
 
--- * Class 'Inj_Modules'
-type Inj_Modules  src ss
- =   Inj_ModulesR src ss ss
+-- * Class 'ModulesInj'
+type ModulesInj  src ss
+ =   ModulesInjR src ss ss
 
-inj_Modules ::
+modulesInj ::
  forall src ss.
- Inj_Modules src ss =>
+ ModulesInj src ss =>
  Either Error_Module (Modules src ss)
-inj_Modules = inj_ModulesR @_ @_ @ss
+modulesInj = modulesInjR @_ @_ @ss
 
--- ** Class 'Inj_ModulesR'
-class Inj_ModulesR src (ss::[*]) (rs::[*]) where
-	inj_ModulesR :: Either Error_Module (Modules src ss)
-instance Inj_ModulesR src ss '[] where
-	inj_ModulesR = Right $ Modules mempty
+-- ** Class 'ModulesInjR'
+class ModulesInjR src (ss::[*]) (rs::[*]) where
+	modulesInjR :: Either Error_Module (Modules src ss)
+instance ModulesInjR src ss '[] where
+	modulesInjR = Right $ Modules mempty
 instance
  ( ModuleFor src ss s
- , Inj_ModulesR src ss rs
- ) => Inj_ModulesR src ss (Proxy s ': rs) where
-	inj_ModulesR = do
-		x <- inj_ModulesR @_ @_ @rs
+ , ModulesInjR src ss rs
+ ) => ModulesInjR src ss (Proxy s ': rs) where
+	modulesInjR = do
+		x <- modulesInjR @_ @_ @rs
 		let (n, m) = moduleFor @_ @_  @s
 		Modules (Map.singleton n m) `unionModules` x
 
@@ -269,58 +220,48 @@
 -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
 lookupDefTerm ::
  forall src ss fixy.
- FixitySing fixy ->
- Imports ->
+ Fixy (ModuleFixy src ss Unifix)
+      (ModuleFixy src ss Infix)
+      (ModuleFixy src ss Unifix)
+      (ModuleFixy src ss fixy) ->
+ Imports NameTe ->
  Mod NameTe ->
  Modules src ss ->
- Either Error_Module (Tokenizer fixy src ss)
-lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
+ Either Error_Module (Tokenizer src ss fixy)
+lookupDefTerm FixyInfix _is ([] `Mod` " ") _ms =
 	Right $ Tokenizer
 	 { token_term   = Token_Term_App @src @ss
 	 , token_fixity = Infix (Just AssocL) 9
 	 }
-lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =
-	let mod_fixy = module_fixity fixy in
-	case Map.lookup m is of
-	 Nothing ->
-		maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=
-		maybe (Left $ Error_Module_missing_Term mn) Right .
-		Map.lookup n . mod_fixy
-	 Just ims ->
-		let look =
-		 -- n matches amongst ims
-			(`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe
-				Map.lookup im mods >>=
-				Map.lookup n . mod_fixy >>=
-				Just . Map.singleton n in
-		case Map.minView look of
-		 Nothing -> Left $ Error_Module_missing_Term mn
-		 Just (r, rs) | null rs -> Right $ snd $ Map.findMin r
-		              | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look
+lookupDefTerm fixy imps mn@(m `Mod` n) (Modules mods) =
+	let m' = m `fromMaybe` lookupImports fixy mn imps in
+	maybe (Left $ Error_Module_missing m') Right (Map.lookup m' mods) >>=
+	maybe (Left $ Error_Module_missing_Term mn) Right .
+	Map.lookup n . selectByFixity fixy
 
 -- | Delete given 'Mod' 'NameTe' into given 'Modules'.
 deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
 deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 	where del mod = mod
-		 { module_prefix  = Map.delete n $ module_prefix  mod
-		 , module_infix   = Map.delete n $ module_infix   mod
-		 , module_postfix = Map.delete n $ module_postfix mod
+		 { byPrefix  = Map.delete n $ byPrefix  mod
+		 , byInfix   = Map.delete n $ byInfix   mod
+		 , byPostfix = Map.delete n $ byPostfix mod
 		 }
 
--- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
+-- | Delete given 'Mod' 'NameTe' into 'byInfix's of given 'Modules'.
 deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
 deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
-	where del mod = mod{module_infix = Map.delete n $ module_infix mod}
+	where del mod = mod{byInfix = Map.delete n $ byInfix mod}
 
--- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
+-- | Delete given 'Mod' 'NameTe' into 'byPrefix's of given 'Modules'.
 deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
 deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
-	where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}
+	where del mod = mod{byPrefix = Map.delete n $ byPrefix mod}
 
--- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
+-- | Delete given 'Mod' 'NameTe' into 'byPostfix's of given 'Modules'.
 deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
 deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
-	where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}
+	where del mod = mod{byPostfix = Map.delete n $ byPostfix mod}
 
 insertDefTerm ::
  forall src ss.
@@ -348,36 +289,6 @@
  Fixity -> Module src ss -> Module src ss
 insertFixity ins fx mod =
 	case fx of
-	 Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
-	 Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
-	 Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
-
--- ** Type 'WithFixity'
-data WithFixity a
- =   WithFixity a Fixity
- deriving (Eq, Show)
-instance IsString (WithFixity NameTe) where
-	fromString a = WithFixity (fromString a) (Fixity2 infixN5)
-
-withInfix :: a -> Infix -> WithFixity a
-withInfix a inf = a `WithFixity` Fixity2 inf
-withInfixR :: a -> Precedence -> WithFixity a
-withInfixR a p = a `WithFixity` Fixity2 (infixR p)
-withInfixL :: a -> Precedence -> WithFixity a
-withInfixL a p = a `WithFixity` Fixity2 (infixL p)
-withInfixN :: a -> Precedence -> WithFixity a
-withInfixN a p = a `WithFixity` Fixity2 (infixN p)
-withInfixB :: a -> (Side, Precedence) -> WithFixity a
-withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
-withPrefix :: a -> Precedence -> WithFixity a
-withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
-withPostfix :: a -> Precedence -> WithFixity a
-withPostfix a p = a `WithFixity` Fixity1 (Postfix p)
-
--- ** Type 'FixitySing'
-data FixitySing fixy where
- FixitySing_Prefix  :: FixitySing Unifix
- FixitySing_Infix   :: FixitySing Infix
- FixitySing_Postfix :: FixitySing Unifix
-deriving instance Eq (FixitySing fixy)
-deriving instance Show (FixitySing fixy)
+	 Fixity1 uni@Prefix{}  -> mod {byPrefix  = ins uni $ byPrefix  mod}
+	 Fixity2 inf@Infix{}   -> mod {byInfix   = ins inf $ byInfix   mod}
+	 Fixity1 uni@Postfix{} -> mod {byPostfix = ins uni $ byPostfix mod}
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
@@ -15,20 +15,21 @@
 -- | Convenient type alias for 'readTerm' and related functions.
 type ReadTerm src ss ts =
  Source src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (KindK src) src =>
- Inj_Source (AST_Type src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (KindK src) src =>
+ SourceInj (AST_Type src) src =>
  Constable (->) =>
- Name2Type src ->
+ 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 n2t ctxTy ast = do
+readTerm impsTy modsTy ctxTy ast = do
 	ts <- go ctxTy `traverse` ast
-	inj_Error `left` betaTerms ts
+	errorInj `left` betaTerms ts
 	where
 	go ::
 	 forall ts'.
@@ -40,12 +41,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 <- inj_Error `left` readType n2t ast_ty_arg
-		when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->
+		TypeVT ty_arg <- errorInj `left` readType impsTy modsTy 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 n2t (CtxTyS name_arg ta ts) ast_body
+				TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name_arg ta ts) ast_body
 				let (qa', qr') = appendVars qa qr
 				let (ta', tr') = appendVars ta tr
 				Right $
@@ -64,11 +65,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 n2t ts ast_arg
+		TermVT (Term qa ta (TeSym arg)) <- readTerm impsTy modsTy ts ast_arg
 		case lenVars ta of
 		 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
 		 LenZ -> do
-			TermVT (Term qr tr (TeSym res)) <- readTerm n2t (CtxTyS name ta ts) ast_body
+			TermVT (Term qr tr (TeSym res)) <- readTerm impsTy modsTy (CtxTyS name ta ts) ast_body
 			let (qa', qr') = appendVars qa qr
 			let tr' = allocVarsL (lenVars ta) tr
 			Right $
@@ -137,12 +138,13 @@
 readTermWithCtx ::
  Foldable f =>
  Source src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (KindK src) src =>
- Inj_Source (AST_Type src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (KindK src) src =>
+ SourceInj (AST_Type src) src =>
  Constable (->) =>
  f (NameTe, TermT src ss '[] '[]) ->
- Name2Type src ->
+ Imports NameTy ->
+ ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
 readTermWithCtx env =
@@ -165,8 +167,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 n2t ctxTy ast = do
-	TermVT (Term q t (TeSym te)) <- readTe n2t (CtxTyS n (qn #> tn) ctxTy) ast
+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
 	case proveConstraint qn of
 	 Nothing -> Left $ Error_Term_proofless $ TypeVT qn
 	 Just Dict ->
@@ -178,15 +180,38 @@
 readTermWithCtxClose ::
  (forall ts'. ReadTerm src ss ts') ->
  Source src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (KindK src) src =>
- Inj_Source (AST_Type src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (KindK src) src =>
+ SourceInj (AST_Type src) src =>
  Constable (->) =>
- Name2Type src ->
+ Imports NameTy ->
+ ModulesTy src ->
  AST_Term src ss ->
  Either (Error_Term src) (TermVT src ss '[])
-readTermWithCtxClose readTe n2t = readTe n2t CtxTyZ
+readTermWithCtxClose readTe impsTy modsTy = readTe impsTy modsTy CtxTyZ
 
+-- * Type 'CtxTy'
+-- | /Typing context/
+-- accumulating at each /lambda abstraction/
+-- the 'Type' of the introduced variable.
+-- It is built top-down from the closest
+-- including /lambda abstraction/ to the farest.
+-- It determines the 'Type's of 'CtxTe'.
+data CtxTy src (ts::[K.Type]) where
+	CtxTyZ :: CtxTy src '[]
+	CtxTyS :: NameTe
+	       -> Type  src '[] t
+	       -> CtxTy src ts
+	       -> CtxTy src (t ': ts)
+infixr 5 `CtxTyS`
+
+appendCtxTy ::
+ CtxTy src ts0 ->
+ CtxTy src ts1 ->
+ CtxTy src (ts0 ++ ts1)
+appendCtxTy CtxTyZ c          = c
+appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
+
 -- * Type 'Error_Term'
 data Error_Term src
  =   Error_Term_unknown NameTe
@@ -198,12 +223,12 @@
  {-   Error_Term_Con_Type (Con_Type src ss) -}
  {-   Error_Term_Con_Kind (Con_Kind src) -}
  deriving (Eq, Show)
-instance Inj_Error (Error_Type src) (Error_Term src) where
-	inj_Error = Error_Term_Type
-instance Inj_Error (Error_Beta src) (Error_Term src) where
-	inj_Error = Error_Term_Beta
-instance Inj_Error (Con_Kind src) (Error_Term src) where
-	inj_Error = Error_Term_Type . inj_Error
+instance ErrorInj (Error_Type src) (Error_Term src) where
+	errorInj = Error_Term_Type
+instance ErrorInj (Error_Beta src) (Error_Term src) where
+	errorInj = Error_Term_Beta
+instance ErrorInj (Con_Kind src) (Error_Term src) where
+	errorInj = Error_Term_Type . errorInj
 
 -- * Type 'SrcTe'
 -- | A 'Source' usable when using 'readTerm'.
@@ -221,13 +246,13 @@
 
 instance Source (SrcTe inp ss) where
 	noSource = SrcTe_Less
-instance Inj_Source (Span inp) (SrcTe inp ss) where
-	inj_Source = SrcTe_Input
-instance Inj_Source (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where
-	inj_Source = SrcTe_AST_Term
-instance Inj_Source (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where
-	inj_Source = SrcTe_AST_Type
-instance Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss) where
-	inj_Source = SrcTe_Kind
-instance Inj_Source (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where
-	inj_Source = SrcTe_Type
+instance SourceInj (Span inp) (SrcTe inp ss) where
+	sourceInj = SrcTe_Input
+instance SourceInj (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where
+	sourceInj = SrcTe_AST_Term
+instance SourceInj (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where
+	sourceInj = SrcTe_AST_Type
+instance SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss) where
+	sourceInj = SrcTe_Kind
+instance SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where
+	sourceInj = SrcTe_Type
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
@@ -52,8 +52,8 @@
 	expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
 
 -- Type
-instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
-	typeOf t = typeOfTerm t `source` TermT t
+instance SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
+	typeOf t = typeOfTerm t `withSource` TermT t
 
 typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
 typeOfTerm (Term q t _) = q #> t
@@ -111,13 +111,13 @@
  )
 
 -- | Like 'TeSym', but 'CtxTe'-free
--- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.
+-- and using 'symInj' to be able to use 'Sym'@ s@ inside.
 teSym ::
  forall s ss ts t.
- Inj_Sym ss s =>
- (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
+ SymInj ss s =>
+ (forall term. Sym s term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
  TeSym ss ts t
-teSym t = inj_Sym @s (TeSym $ const t)
+teSym t = symInj @s (TeSym $ const t)
 
 -- ** Type family 'QualOf'
 -- | Qualification
@@ -166,39 +166,39 @@
 
 -- ** Type 'TermDef'
 -- | Convenient type alias for defining 'Term'.
-type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t
+type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
 
 -- ** Type family 'Sym'
-type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
+type family Sym (s::k) :: {-term-}(K.Type -> K.Type) -> Constraint
 
 -- ** Type family 'Syms'
-type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
+type family Syms (ss::[K.Type]) (term::K.Type -> K.Type) :: Constraint where
 	Syms '[] term = ()
-	Syms (s ': ss) term = (Sym s term, Syms ss term)
+	Syms (Proxy s ': ss) term = (Sym s term, Syms ss term)
 
--- ** Type 'Inj_Sym'
--- | Convenient type synonym wrapping 'Inj_SymP'
+-- ** Type 'SymInj'
+-- | Convenient type synonym wrapping 'SymPInj'
 -- applied on the correct 'Index'.
-type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
+type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s
 
 -- | Inject a given /symantic/ @s@ into a list of them,
 -- by returning a function which given a 'TeSym' on @s@
 -- returns the same 'TeSym' on @ss@.
-inj_Sym ::
+symInj ::
  forall s ss ts t.
- Inj_Sym ss s =>
+ SymInj ss s =>
  TeSym '[Proxy s] ts t ->
  TeSym ss ts t
-inj_Sym = inj_SymP @(Index ss (Proxy s))
+symInj = symInjP @(Index ss (Proxy s))
 
--- *** Class 'Inj_SymP'
-class Inj_SymP p ss s where
-	inj_SymP :: TeSym '[Proxy s] ts t -> TeSym ss ts t
-instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
-	inj_SymP (TeSym te) = TeSym te
-instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
-	inj_SymP (te::TeSym '[Proxy s] ts t) =
-		case inj_SymP @p te :: TeSym ss ts t of
+-- *** Class 'SymPInj'
+class SymInjP p ss s where
+	symInjP :: TeSym '[Proxy s] ts t -> TeSym ss ts t
+instance SymInjP Zero (Proxy s ': ss) (s::k) where
+	symInjP (TeSym te) = TeSym te
+instance SymInjP p ss s => SymInjP (Succ p) (Proxy not_s ': ss) s where
+	symInjP (te::TeSym '[Proxy s] ts t) =
+		case symInjP @p te :: TeSym ss ts t of
 		 TeSym te' -> TeSym te'
 
 -- * Class 'Sym_Lambda'
diff --git a/Language/Symantic/Typing.hs b/Language/Symantic/Typing.hs
--- a/Language/Symantic/Typing.hs
+++ b/Language/Symantic/Typing.hs
@@ -4,6 +4,7 @@
  , module Language.Symantic.Typing.Peano
  , module Language.Symantic.Typing.Kind
  , module Language.Symantic.Typing.Variable
+ , module Language.Symantic.Typing.Module
  , module Language.Symantic.Typing.Type
  , module Language.Symantic.Typing.Grammar
  , module Language.Symantic.Typing.Document
@@ -16,6 +17,7 @@
 import Language.Symantic.Typing.Peano
 import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.Module
 import Language.Symantic.Typing.Type
 import Language.Symantic.Typing.Grammar
 import Language.Symantic.Typing.Document
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
@@ -4,9 +4,9 @@
 
 import Data.Function (id)
 import Data.Map.Strict (Map)
+import Data.Maybe (fromMaybe)
 import Data.Semigroup (Semigroup(..))
 import Data.Set (Set)
-import Data.Text (Text)
 import Data.Typeable
 import qualified Data.List as L
 import qualified Data.Map.Strict as Map
@@ -17,10 +17,11 @@
 import Language.Symantic.Grammar
 import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.Module
 import Language.Symantic.Typing.Type
 
 -- * Type 'Config_Doc_Type'
-newtype Config_Doc_Type
+data Config_Doc_Type
  =   Config_Doc_Type
  {   config_Doc_Type_vars_numbering :: Bool
      -- ^ Style of /type variables/:
@@ -29,13 +30,17 @@
      -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
      --
      -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
+ ,   config_Doc_Type_imports :: Imports NameTy
  }
 
-config_doc_type :: Config_Doc_Type
-config_doc_type =
+config_Doc_Type :: Config_Doc_Type
+config_Doc_Type =
 	Config_Doc_Type
-	 { config_Doc_Type_vars_numbering = True }
+	 { config_Doc_Type_vars_numbering = True
+	 , config_Doc_Type_imports        = mempty
+	 }
 
+-- * Document 'Type'
 docType ::
  forall src vs t d.
  Semigroup d =>
@@ -44,7 +49,7 @@
  Config_Doc_Type ->
  Precedence ->
  Type src vs t -> d
-docType conf pr ty =
+docType conf@Config_Doc_Type{config_Doc_Type_imports=imps} pr ty =
 	let (v2n, _) = var2Name conf mempty ty in
 	go v2n (infixB SideL pr, SideL) ty
 	where
@@ -53,18 +58,23 @@
 	 (Map IndexVar Name) -> -- names of variables
 	 (Infix, Side) ->
 	 Type src vs x -> d
-	go _v2n _po c
-	 | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"
-	go _v2n _po (TyConst _src _vs c) = D.stringH $ show c
+	-- Var
 	go v2n _po (TyVar _src _n v) =
 		let iv = indexVar v in
 		case Map.lookup iv v2n of
 		 Nothing -> error "[BUG] docType: variable name missing"
 		 Just n -> D.textH n
+	-- Const
+	go _v2n _po (TyConst _src _vs c@Const{}) =
+		(if isNameTyOp c then D.paren else id) $
+		docConst imps c
+	-- [] Const
 	go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
 	 | Just HRefl <- proj_ConstKi @(K []) @[] f =
 		"[" <> go v2n (infixB SideL 0, SideL) a <> "]"
+	-- Infix Const
 	go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
+	 -- () =>
 	 | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
 	 , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
 		go v2n po b
@@ -75,8 +85,6 @@
 		go v2n (op, SideR) b
 		where
 		d_op = D.yellower
-		unParen ('(':s) | ')':s' <- reverse s = reverse s'
-		unParen s = s
 		prettyConst :: forall k c. Const src (c::k) -> d
 		prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
 		prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> D.space
@@ -89,41 +97,23 @@
 		 -- NOTE: cannot use 'proj_ConstKi' here
 		 -- because (#~) has a polymorphic kind.
 		 = D.space <> d_op "~" <> D.space
-		 | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space
+		 | otherwise = D.space <> d_op (docConst imps c) <> D.space
+	-- TyApp
 	go v2n po (TyApp _src f a) =
 		let op = infixL 11 in
 		(if needsParenInfix po op then D.paren else id) $
 		go v2n (op, SideL) f <>
 		D.space <>
 		go v2n (op, SideR) a
+	-- TyFam
 	go v2n po (TyFam _src _len fam args) =
 		let op = infixL 11 in
 		(if needsParenInfix po op then D.paren else id) $
-		D.stringH (show fam) <>
+		docConst imps fam <>
 		foldlTys (\t acc ->
 			D.space <> go v2n (op, SideL) t <> acc
 		 ) args D.empty
 
-docTypes ::
- forall src vs ts d.
- Semigroup d =>
- D.Doc_Text d =>
- D.Doc_Color d =>
- Config_Doc_Type ->
- Types src vs ts -> d
-docTypes conf tys =
-	d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
-	where
-	d_op = D.yellower
-	go :: forall xs. Types src vs xs -> d
-	go TypesZ = D.empty
-	go (TypesS t0 (TypesS t1 ts)) =
-		docType conf 10 t0 <>
-		d_op (D.charH ',') <> D.space <>
-		docType conf 10 t1 <>
-		go ts
-	go (TypesS t ts) = docType conf 10 t <> go ts
-
 -- | Return a 'Map' associating a distinct 'Name'
 -- for all the variables of the given 'Type'.
 var2Name ::
@@ -147,10 +137,8 @@
 var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
 var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st
 
--- ** Type 'Name'
-type Name     = Text
-type NameHint = Name
-type Names    = Set Name
+-- ** Type 'Names'
+type Names = Set Name
 
 -- | Return given 'Name' renamed a bit to avoid
 -- conflicting with any given 'Names'.
@@ -175,3 +163,141 @@
 	[ T.singleton n     | n <- ['a'..'z'] ] <>
 	[ T.pack (n:show i) | n <- ['a'..'z']
 	                    , i <- [1 :: Int ..] ]
+
+-- * Document 'Types'
+docTypes ::
+ forall src vs ts d.
+ Semigroup d =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ Config_Doc_Type ->
+ Types src vs ts -> d
+docTypes conf tys =
+	d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
+	where
+	d_op = D.yellower
+	go :: forall xs. Types src vs xs -> d
+	go TypesZ = D.empty
+	go (TypesS t0 (TypesS t1 ts)) =
+		docType conf 10 t0 <>
+		d_op (D.charH ',') <> D.space <>
+		docType conf 10 t1 <>
+		go ts
+	go (TypesS t ts) = docType conf 10 t <> go ts
+
+-- * Document 'Const'
+docConst :: D.Doc_Text d => Imports NameTy -> Const src c -> d
+docConst imps c@Const{} =
+	docMod docNameTy $
+	maybe mn (`Mod` n) $
+	revlookupImports f (m `Mod` n) imps
+	where
+	f = fixyOfFixity $ Fixity2 infixN5 `fromMaybe` fixityOf c
+	mn@(m `Mod` n) = nameTyOf c
+
+-- * Document 'NameTy'
+docNameTy :: D.Doc_Text d => NameTy -> d
+docNameTy (NameTy t) = D.textH t
+
+-- * Document 'Mod'
+docMod :: D.Doc_Text d => (a -> d) -> Mod a -> d
+docMod a2d ([] `Mod` a) = a2d a
+docMod a2d (m `Mod`  a) = docPathMod m <> (D.charH '.') <> a2d a
+
+-- * Document 'PathMod'
+docPathMod :: D.Doc_Text d => PathMod -> d
+docPathMod (p::PathMod) =
+	D.catH $
+	L.intersperse (D.charH '.') $
+	(\(NameMod n) -> D.textH n) <$> p
+
+
+{-
+docModules ::
+ Source src =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ D.Doc_Decoration d =>
+ ReadTe src ss =>
+ Sym.Modules src ss -> d
+docModules (Sym.Modules mods) =
+	Map.foldrWithKey
+	 (\p m doc -> docModule p m <> doc)
+	 D.empty
+	 mods
+
+docModule ::
+ forall src ss d.
+ Source src =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ D.Doc_Decoration d =>
+ ReadTe src ss =>
+ Sym.PathMod -> Sym.Module src ss -> d
+docModule m Sym.Module
+ { Sym.module_infix
+ , Sym.module_prefix
+ , Sym.module_postfix
+ } =
+	go docFixityInfix   module_infix <>
+	go docFixityPrefix  module_prefix <>
+	go docFixityPostfix module_postfix
+	where
+	go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
+	go docFixy =
+		Map.foldrWithKey
+		 (\n Sym.Tokenizer
+			 { Sym.token_fixity
+			 , Sym.token_term = t
+			 } doc ->
+			docPathTe m n <>
+			docFixy token_fixity <>
+			D.space <> D.bold (D.yellower "::") <> D.space <>
+			docTokenTerm (t Sym.noSource) <>
+			D.eol <> doc)
+		 D.empty
+
+docTokenTerm ::
+ forall src ss d.
+ Source src =>
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ ReadTe src ss =>
+ Sym.Token_Term src ss -> d
+docTokenTerm t =
+	let n2t = name2typeInj @ss in
+	case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of
+	 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
+	 Right (Sym.TermVT te) ->
+		Sym.docType Sym.config_doc_type
+		 { config_Doc_Type_vars_numbering = False
+		 } 0 $ Sym.typeOfTerm te
+
+docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
+docFixityInfix = \case
+	 Sym.Infix Nothing 5 -> D.empty
+	 Sym.Infix a p ->
+		let docAssoc = \case
+			 Sym.AssocL -> "l"
+			 Sym.AssocR -> "r"
+			 Sym.AssocB Sym.SideL -> "l"
+			 Sym.AssocB Sym.SideR -> "r" in
+		D.magenta $ " infix" <> maybe D.empty docAssoc a <>
+		D.space <> D.bold (D.bluer (D.int p))
+docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
+docFixityPrefix p = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
+docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
+docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
+
+docPathTe ::
+ D.Doc_Text d =>
+ D.Doc_Color d =>
+ Sym.PathMod -> Sym.NameTe -> d
+docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
+	D.catH $
+	L.intersperse (D.charH '.') $
+	((\(Sym.NameMod m) -> D.textH m) <$> ms) <>
+	[(if isOp n then id else D.yellower) $ D.text n]
+	where
+	isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
+-}
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
@@ -1,3 +1,5 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -5,32 +7,29 @@
 
 import Control.Applicative (Applicative(..))
 import Data.List (foldl1')
+import Data.Proxy (Proxy(..))
+import Data.Semigroup (Semigroup(..))
 import Data.String (IsString(..))
-import Data.Text (Text)
+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 Language.Symantic.Grammar
+import Language.Symantic.Grammar as G
+import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Variable
-
--- * Type 'NameTy'
-newtype NameTy = NameTy Text
- deriving (Eq, Ord, Show)
-instance IsString NameTy where
-	fromString = NameTy . fromString
-
--- ** Type 'NameConst'
-type NameConst = NameTy
-
--- ** Type 'NameFam'
-type NameFam = NameTy
+import Language.Symantic.Typing.List
+import Language.Symantic.Typing.Module
+import Language.Symantic.Typing.Type
 
 -- * Type 'AST_Type'
 -- | /Abstract Syntax Tree/ of 'Token_Type'.
-type AST_Type src = BinTree (Token_Type src) -- (EToken src '[Proxy K.Type])
+type AST_Type src = BinTree (Token_Type src)
 
 -- ** Type 'Token_Type'
 data Token_Type src
- =   Token_Type_Const (At src NameTy)
+ =   Token_Type_Const (At src (Mod NameTy))
  |   Token_Type_Var   (At src NameVar)
  -- deriving (Eq, Show)
 instance Source src => Eq (Token_Type src) where
@@ -47,6 +46,133 @@
 		showString "Token_Type_Var" .
 		showChar ' ' . showsPrec 10 x
 
+-- * Type 'ModulesTy'
+type ModulesTy src = Map (Mod NameTy) (TypeTLen src)
+
+-- ** Type 'TypeTLen'
+-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
+--
+-- Useful to build a 'ModulesTy' which can be used
+-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
+newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
+instance Source src => Eq (TypeTLen src) where
+	TypeTLen x == TypeTLen y = x LenZ == y LenZ
+instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where
+	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
+
+-- ** Class 'ModulesTyInj'
+-- | Derive a 'ModulesTy' from the given type-level list
+-- of 'Proxy'-fied /type constants/.
+class ModulesTyInj ts where
+	modulesTyInj :: Source src => ModulesTy src
+instance ModulesTyInj '[] where
+	modulesTyInj = Map.empty
+instance
+ ( KindInjP (Ty_of_Type (K c))
+ , K c ~ Type_of_Ty (Ty_of_Type (K c))
+ , Constable c
+ , ModulesTyInj ts
+ ) => ModulesTyInj (Proxy c ': ts) where
+	modulesTyInj =
+		Map.insert
+		 (nameTyOf $ Proxy @c)
+		 (TypeTLen $ \len -> TypeT $ TyConst noSource len $
+			constKiInj @(K c) @c $
+			kindInjP @(Ty_of_Type (K c)) noSource) $
+		modulesTyInj @ts
+
+
+-- * Class 'Gram_Mod'
+class
+ ( Gram_Terminal g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ ) => Gram_Mod g where
+	g_PathMod :: CF g PathMod
+	g_PathMod = rule "PathMod" $
+		infixrG
+		 (pure <$> g_NameMod)
+		 (op <$ char '.')
+		where op = (<>)
+	g_NameMod :: CF g NameMod
+	g_NameMod = rule "NameMod" $
+		NameMod . Text.pack <$> identG
+		where
+		identG = (:) <$> headG <*> many (cfOf tailG)
+		headG = unicat $ Unicat Char.UppercaseLetter
+		tailG :: Terminal g Char
+		tailG =
+			unicat Unicat_Letter <+>
+			unicat Unicat_Number
+
+deriving instance Gram_Mod g => Gram_Mod (CF g)
+instance Gram_Mod EBNF
+instance Gram_Mod RuleEBNF
+
+-- * Class 'Gram_Type_Name'
+class
+ ( Gram_Terminal g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ , Gram_Mod g
+ ) => Gram_Type_Name g where
+	g_ModNameTy :: CF g (Mod NameTy)
+	g_ModNameTy = rule "ModNameTy" $
+		lexeme $
+			g_ModNameTyId <+>
+			parens g_ModNameTyOp
+	
+	g_ModNameTyId :: CF g (Mod NameTy)
+	g_ModNameTyId = rule "ModNameTyId" $
+		Mod
+		 <$> option [] (try $ g_PathMod <* char '.')
+		 <*> g_NameTyId
+	g_NameTyId :: CF g NameTy
+	g_NameTyId = rule "NameTyId" $
+		NameTy . Text.pack <$> identTyG
+		where
+		identTyG = (:) <$> headTyG <*> many (cfOf tailTyG)
+		headTyG = unicat $ Unicat Char.UppercaseLetter
+		tailTyG :: Terminal g Char
+		tailTyG =
+			unicat Unicat_Letter <+>
+			unicat Unicat_Number
+	
+	g_ModNameTyOp :: CF g (Mod NameTy)
+	g_ModNameTyOp = rule "ModNameTyOp" $
+		Mod
+		 <$> option [] (try $ g_PathMod <* char '.')
+		 <*> g_NameTyOp
+	g_NameTyOp :: CF g NameTy
+	g_NameTyOp = rule "NameTyOp" $
+		NameTy . Text.pack <$> many (cfOf okG)
+		where
+		okG :: Terminal g Char
+		okG = choice (unicat <$>
+			 [ Unicat_Symbol
+			 , Unicat_Punctuation
+			 , Unicat_Mark
+			 ]) `but` koG
+		koG = choice (char <$> ['(', ')', '`', '\'', '[', ']'])
+
+deriving instance Gram_Type_Name g => Gram_Type_Name (CF g)
+instance Gram_Type_Name EBNF
+instance Gram_Type_Name RuleEBNF
+
 -- * Class 'Gram_Type'
 -- | Read an 'AST_Type' from a textual source.
 class
@@ -60,27 +186,31 @@
  , Gram_CF g
  , Gram_Comment g
  , Gram_Op g
+ , Gram_Type_Name g
+ , NameTyOf (->)
+ , NameTyOf []
+ , NameTyOf (,)
  ) => 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 (g_source $ op <$ symbol "->")
-		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(->)")
+		infixrG g_type_list (source $ op <$ symbol "->")
+		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(->))
 	-- 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_source $ inside mk
+		source $ inside mk
 		 (symbol "[") (optional g_type) (symbol "]")
 		 (const <$> g_type_tuple2)
 		where
 		mk Nothing  src = tok src
 		mk (Just a) src = BinTree2 (tok src) a
-		tok src = BinTree0 $ Token_Type_Const $ At src "[]"
+		tok src = BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @[]
 	g_type_tuple2 :: CF g (AST_Type src)
 	g_type_tuple2 = rule "type_tuple2" $
-		try (parens (infixrG (g_type) (g_source $ op <$ symbol ","))) <+> (g_type_app)
-		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src "(,)")
+		try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
+		where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ At src $ nameTyOf $ Proxy @(,))
 	g_type_app :: CF g (AST_Type src)
 	g_type_app = rule "type_app" $
 		foldl1' BinTree2 <$> some (g_type_atom)
@@ -88,36 +218,49 @@
 	g_type_atom = rule "type_atom" $
 		try (parens g_type) <+>
 		g_type_name_const <+>
-		g_type_name_var <+>
-		g_type_symbol
+		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 $ g_source $
-		(\n ns src -> BinTree0 $ Token_Type_Const $ At src $ fromString $ n:ns)
-		 <$> unicat (Unicat Char.UppercaseLetter)
-		 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
+		lexeme $ source $
+		(\n src -> BinTree0 $ Token_Type_Const $ At 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 $ g_source $
+		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" $
-		g_source $ (mk <$>) $
-		parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
+		source $ (mk <$>) $
+		parens $ many $ cfOf $ choice g_ok `but` choice g_ko
 		where
-		mk s src = BinTree0 $ Token_Type_Const $ At src (fromString $ "(" ++ s ++ ")")
+		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 => Gram_Type src EBNF
-instance Gram_Source src RuleEBNF => Gram_Type src RuleEBNF
+instance
+ ( Gram_Source src EBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
+ ) => Gram_Type src EBNF
+instance
+ ( Gram_Source src RuleEBNF
+ , NameTyOf (->)
+ , NameTyOf (,)
+ , NameTyOf []
+ ) => Gram_Type src RuleEBNF
 
 -- | List of the rules of 'Gram_Type'.
 gram_type :: Gram_Type () g => [CF g (AST_Type ())]
@@ -130,5 +273,5 @@
  , g_type_atom
  , g_type_name_const
  , g_type_name_var
- , g_type_symbol
+ -- , g_type_symbol
  ]
diff --git a/Language/Symantic/Typing/Kind.hs b/Language/Symantic/Typing/Kind.hs
--- a/Language/Symantic/Typing/Kind.hs
+++ b/Language/Symantic/Typing/Kind.hs
@@ -51,33 +51,33 @@
 class KindOf (a::kt -> K.Type) where
 	kindOf :: a t -> Kind (SourceOf (a t)) kt
 
--- * Type 'Inj_Kind'
+-- * Type 'Kind'Inj
 -- | Implicit 'Kind'.
 --
 -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
 -- makes it fail to properly build an implicit 'Kind',
 -- this can however be worked around by having the class instances
 -- work on a data type 'Ty' instead of 'Data.K.Type',
--- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.
-class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where
-instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k
+-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'KindP'.Inj
+class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k where
+instance (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k
 
-inj_Kind ::
+kindInj ::
  forall k src.
  Source src =>
- Inj_Kind k =>
+ KindInj k =>
  Kind src k
-inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src)
+kindInj = kindInjP @(Ty_of_Type k) (noSource @src)
 
--- ** Type 'Inj_KindP'
-class Inj_KindP k where
-	inj_KindP :: src -> Kind src (Type_of_Ty k)
-instance Inj_KindP K.Constraint where
-	inj_KindP = KiConstraint
-instance Inj_KindP Ty where
-	inj_KindP = KiType
-instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where
-	inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src)
+-- ** Type 'KindP'Inj
+class KindInjP k where
+	kindInjP :: src -> Kind src (Type_of_Ty k)
+instance KindInjP K.Constraint where
+	kindInjP = KiConstraint
+instance KindInjP Ty where
+	kindInjP = KiType
+instance (KindInjP a, KindInjP b) => KindInjP (a -> b) where
+	kindInjP src = KiFun src (kindInjP @a src) (kindInjP @b src)
 
 -- ** Type 'Ty'
 -- | FIXME: workaround to be removed when
@@ -118,18 +118,18 @@
  deriving (Eq, Show)
 
 when_EqKind
- :: Inj_Error (Con_Kind src) err
+ :: ErrorInj (Con_Kind src) err
  => Kind src x
  -> Kind src y
  -> ((x :~: y) -> Either err ret) -> Either err ret
 when_EqKind x y k =
 	case x `eqKind` y of
 	 Just Refl -> k Refl
-	 Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)
+	 Nothing -> Left $ errorInj $ Con_Kind_Eq (KindK x) (KindK y)
 
 when_KiFun ::
- Inj_Error (Con_Kind src) err =>
- Inj_Source (KindK src) src =>
+ ErrorInj (Con_Kind src) err =>
+ SourceInj (KindK src) src =>
  Kind src x ->
  (forall a b. (x :~: (a -> b)) ->
               Kind src a ->
@@ -138,5 +138,5 @@
  Either err ret
 when_KiFun x k =
 	case x of
-	 KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
-	 _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)
+	 KiFun _src a b -> k Refl (a `withSource` KindK x) (b `withSource` KindK x)
+	 _ -> Left $ errorInj $ Con_Kind_Arrow (KindK x)
diff --git a/Language/Symantic/Typing/List.hs b/Language/Symantic/Typing/List.hs
--- a/Language/Symantic/Typing/List.hs
+++ b/Language/Symantic/Typing/List.hs
@@ -65,13 +65,13 @@
 	L '[] = 'Z
 	L (x ': xs) = 'S (L xs)
 
--- ** Class 'Inj_L'
-class Inj_L (as::[k]) where
-	inj_L :: SNat (L as)
-instance Inj_L '[] where
-	inj_L = SNatZ
-instance Inj_L as => Inj_L (a ': as) where
-	inj_L = SNatS (inj_L @_ @as)
+-- ** Class 'LInj'
+class LInj (as::[k]) where
+	lInj :: SNat (L as)
+instance LInj '[] where
+	lInj = SNatZ
+instance LInj as => LInj (a ': as) where
+	lInj = SNatS (lInj @_ @as)
 -}
 
 -- * Type 'Len'
@@ -101,10 +101,10 @@
 	go i LenZ     = i
 	go i (LenS l) = go (1 + i) l
 
--- ** Class 'Inj_Len'
-class Inj_Len (vs::[k]) where
-	inj_Len :: Len vs
-instance Inj_Len '[] where
-	inj_Len = LenZ
-instance Inj_Len as => Inj_Len (a ': as) where
-	inj_Len = LenS inj_Len
+-- ** Class 'LenInj'
+class LenInj (vs::[k]) where
+	lenInj :: Len vs
+instance LenInj '[] where
+	lenInj = LenZ
+instance LenInj as => LenInj (a ': as) where
+	lenInj = LenS lenInj
diff --git a/Language/Symantic/Typing/Module.hs b/Language/Symantic/Typing/Module.hs
new file mode 100644
--- /dev/null
+++ b/Language/Symantic/Typing/Module.hs
@@ -0,0 +1,240 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Language.Symantic.Typing.Module where
+
+import Data.Functor (Functor(..))
+import Data.Maybe (fromMaybe)
+import Data.String (IsString(..))
+import Data.Semigroup (Semigroup(..))
+import Data.Text (Text)
+import Data.Typeable
+import Data.Map.Strict (Map)
+import qualified Data.Char as C
+import qualified Data.List as L
+import qualified Data.Kind as K
+import qualified Data.Text as T
+import qualified Data.Map.Strict as Map
+
+import Language.Symantic.Grammar.Fixity
+
+-- * Type 'NsT'
+data NsT
+ =   NsTerm
+ |   NsType
+
+-- * Type 'Name'
+type Name = Text
+
+-- * Type 'NameTy'
+-- | 'Name' of a 'Type'.
+newtype NameTy = NameTy Text
+ deriving (Eq, Ord, Show)
+instance IsString NameTy where
+	fromString = NameTy . fromString
+
+-- ** Type 'NameConst'
+-- | 'Name' of a 'Const'.
+type NameConst = NameTy
+
+-- ** Type 'NameFam'
+-- | 'Name' of a 'Fam'.
+type NameFam = NameTy
+
+-- ** Class 'NameOf'
+class NameOf a where
+	nameOf :: a -> Name
+
+-- ** Class 'NameTyOf'
+-- | Return the 'NameTy' of something.
+class NameTyOf (c::kc) where
+	nameTyOf :: proxy c -> Mod NameTy
+	default nameTyOf :: Typeable c => proxy c -> Mod NameTy
+	nameTyOf c = path (tyConModule repr) `Mod` fromString (tyConName repr)
+		where
+		repr = typeRepTyCon (typeRep c)
+		path = fmap fromString . L.lines . fmap (\case '.' -> '\n'; x -> x)
+	
+	isNameTyOp :: proxy c -> Bool
+	default isNameTyOp :: Typeable c => proxy c -> Bool
+	isNameTyOp c = let _m `Mod` NameTy n = nameTyOf c in isOp n
+		where
+		isOp = T.all $ \case
+			 '_'  -> False
+			 '\'' -> False
+			 x -> case C.generalCategory x of
+				 C.NonSpacingMark       -> True
+				 C.SpacingCombiningMark -> True
+				 C.EnclosingMark        -> True
+				 C.ConnectorPunctuation -> True
+				 C.DashPunctuation      -> True
+				 C.OpenPunctuation      -> True
+				 C.ClosePunctuation     -> True
+				 C.InitialQuote         -> True
+				 C.FinalQuote           -> True
+				 C.OtherPunctuation     -> True
+				 C.MathSymbol           -> True
+				 C.CurrencySymbol       -> True
+				 C.ModifierSymbol       -> True
+				 C.OtherSymbol          -> True
+				 
+				 C.UppercaseLetter      -> False
+				 C.LowercaseLetter      -> False
+				 C.TitlecaseLetter      -> False
+				 C.ModifierLetter       -> False
+				 C.OtherLetter          -> False
+				 C.DecimalNumber        -> False
+				 C.LetterNumber         -> False
+				 C.OtherNumber          -> False
+				 C.Space                -> False
+				 C.LineSeparator        -> False
+				 C.ParagraphSeparator   -> False
+				 C.Control              -> False
+				 C.Format               -> False
+				 C.Surrogate            -> False
+				 C.PrivateUse           -> False
+				 C.NotAssigned          -> False
+
+-- * Type 'Mod'
+-- | 'PathMod' of something.
+data Mod a = Mod PathMod a
+ deriving (Eq, Functor, Ord, Show)
+
+-- ** Type 'PathMod'
+-- | Path to a 'Module'.
+type PathMod = [NameMod]
+
+-- ** Type 'NameMod'
+-- | 'Name' of 'Module'.
+newtype NameMod = NameMod Name
+ deriving (Eq, Ord, Show)
+instance IsString NameMod where
+	fromString = NameMod . fromString
+
+-- * Type 'Imports'
+-- | Map 'PathMod's of 'Name's.
+newtype Imports name = Imports (Map PathMod (MapFixity (Map name PathMod)))
+ deriving (Eq, Show)
+
+instance Ord name => Semigroup (Imports name) where
+	Imports x <> Imports y = Imports $ Map.unionWith (<>) x y
+instance Ord name => Monoid (Imports name) where
+	mempty  = Imports mempty
+	mappend = (<>)
+
+lookupImports :: Ord name => Fixy p i q a -> Mod name -> Imports name -> Maybe PathMod
+lookupImports f (m `Mod` n) (Imports is) =
+	Map.lookup m is >>=
+	Map.lookup n . getByFixity f
+
+revlookupImports :: Ord name => Fixy p i q a -> Mod name -> Imports name -> Maybe PathMod
+revlookupImports f (m `Mod` n) (Imports is) =
+	(fst . fst <$>) $ Map.minViewWithKey $
+	Map.filter (\i ->
+		case Map.lookup n $ getByFixity f i of
+		 Just m' | m' == m -> True
+		 _ -> False
+	 ) is
+
+-- ** Class 'ImportTypes'
+class ImportTypes ts where
+	importTypes :: PathMod -> Imports NameTy
+
+instance ImportTypes '[] where
+	importTypes _p = mempty
+instance (NameTyOf t, FixityOf t, ImportTypes ts) => ImportTypes (Proxy t ': ts) where
+	importTypes p = Imports (Map.singleton p byFixy) <> importTypes @ts p
+		where
+		t = Proxy @t
+		f = Fixity2 infixN5 `fromMaybe` fixityOf t
+		m `Mod` n = nameTyOf t
+		byFixy :: MapFixity (Map NameTy PathMod)
+		byFixy = case f of
+			Fixity1 Prefix{}  -> ByFixity{byPrefix  = Map.singleton n m, byInfix =mempty, byPostfix=mempty}
+			Fixity2{}         -> ByFixity{byInfix   = Map.singleton n m, byPrefix=mempty, byPostfix=mempty}
+			Fixity1 Postfix{} -> ByFixity{byPostfix = Map.singleton n m, byPrefix=mempty, byInfix  =mempty}
+
+-- * Type 'Fixy'
+data Fixy p i q a where
+ FixyPrefix  :: Fixy p i q p
+ FixyInfix   :: Fixy p i q i
+ FixyPostfix :: Fixy p i q q
+deriving instance Eq   (Fixy p i q a)
+deriving instance Show (Fixy p i q a)
+
+fixyOfFixity :: Fixity -> Fixy a a a a
+fixyOfFixity (Fixity1 Prefix{})  = FixyPrefix
+fixyOfFixity (Fixity2 Infix{})   = FixyInfix
+fixyOfFixity (Fixity1 Postfix{}) = FixyPostfix
+
+-- ** Class 'FixityOf'
+-- | Return the 'Fixity' of something.
+class FixityOf (c::kc) where
+	fixityOf :: proxy c -> Maybe Fixity
+	fixityOf _c = Nothing
+instance FixityOf (c::K.Type)
+instance FixityOf (c::K.Constraint)
+
+-- ** Type 'FixyA'
+-- | Like 'Fixy', but when all choices have the same type.
+newtype FixyA = FixyA (forall (a:: *). Fixy a a a a)
+deriving instance Eq   FixyA
+deriving instance Show FixyA
+
+-- ** Type 'WithFixity'
+data WithFixity a
+ =   WithFixity a Fixity
+ deriving (Eq, Functor, Show)
+instance IsString a => IsString (WithFixity a) where
+	fromString a = WithFixity (fromString a) (Fixity2 infixN5)
+
+withInfix :: a -> Infix -> WithFixity a
+withInfix a inf = a `WithFixity` Fixity2 inf
+withInfixR :: a -> Precedence -> WithFixity a
+withInfixR a p = a `WithFixity` Fixity2 (infixR p)
+withInfixL :: a -> Precedence -> WithFixity a
+withInfixL a p = a `WithFixity` Fixity2 (infixL p)
+withInfixN :: a -> Precedence -> WithFixity a
+withInfixN a p = a `WithFixity` Fixity2 (infixN p)
+withInfixB :: a -> (Side, Precedence) -> WithFixity a
+withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
+withPrefix :: a -> Precedence -> WithFixity a
+withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
+withPostfix :: a -> Precedence -> WithFixity a
+withPostfix a p = a `WithFixity` Fixity1 (Postfix p)
+
+-- ** Type 'ByFixity'
+-- | Fixity namespace.
+data ByFixity p i q
+ =   ByFixity
+ {   byPrefix  :: p
+ ,   byInfix   :: i
+ ,   byPostfix :: q
+ } deriving (Eq, Show)
+instance (Semigroup p, Semigroup i, Semigroup q) => Semigroup (ByFixity p i q) where
+	ByFixity px ix qx <> ByFixity py iy qy =
+		ByFixity (px <> py) (ix <> iy) (qx <> qy)
+instance (Monoid p, Monoid i, Monoid q) => Monoid (ByFixity p i q) where
+	mempty = ByFixity mempty mempty mempty
+	ByFixity px ix qx `mappend` ByFixity py iy qy =
+		ByFixity (px `mappend` py) (ix `mappend` iy) (qx `mappend` qy)
+
+getByFixity :: Fixy p i q a -> MapFixity b -> b
+getByFixity FixyPrefix  = byPrefix
+getByFixity FixyInfix   = byInfix
+getByFixity FixyPostfix = byPostfix
+
+selectByFixity :: Fixy p i q a -> ByFixity p i q -> a
+selectByFixity FixyPrefix  = byPrefix
+selectByFixity FixyInfix   = byInfix
+selectByFixity FixyPostfix = byPostfix
+
+-- *** Type 'MapFixity'
+-- | Like 'ByFixity', but with the same type parameter.
+type MapFixity a = ByFixity a a a
+
+mapMapFixity :: (a -> b) -> MapFixity a -> MapFixity b
+mapMapFixity f (ByFixity p i q) = ByFixity (f p) (f i) (f q)
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,10 +2,9 @@
 {-# LANGUAGE PolyKinds #-}
 module Language.Symantic.Typing.Read where
 
-import Data.Map.Strict (Map)
+import Data.Maybe (fromMaybe)
 import Data.Typeable
 import qualified Data.Map.Strict as Map
-import qualified Data.Text as Text
 
 import Language.Symantic.Grammar
 import Language.Symantic.Typing.List
@@ -14,51 +13,56 @@
 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 ::
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ 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 cs ast | EVars vs <- readVars (EVars VarsZ) ast = do
-	TypeT ty <- readTyVars cs vs ast
+readType is ms ast | EVars vs <- readVars (EVars VarsZ) ast = do
+	TypeT ty <- readTyVars is ms vs ast
 	Right $ TypeVT ty
 
 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
 readTyVars ::
  forall vs src.
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ 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 cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
-	readTyName cs (inj_Source ast) (lenVars vs) name
-readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
+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))) =
 	case lookupVars name vs of
-	 Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
+	 Just (EVar v) -> Right $ TypeT $ TyVar (sourceInj ast) name v
 	 Nothing -> error "[BUG] readTyVars: lookupVars failed"
-readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
-	TypeT ty_x <- readTyVars cs vs ast_x
-	TypeT ty_y <- readTyVars cs vs ast_y
+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
 	when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
 		when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
-			Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y
+			Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
 
 -- | Lookup a 'TyConst' or 'Type' synonym
--- associated with given 'NameTy' in given 'Name2Type',
+-- associated with given 'NameTy' in given 'ModulesTy',
 -- building it for a @vs@ of given 'Len'.
 readTyName ::
  Source src =>
- Name2Type src -> src -> Len vs -> NameTy ->
+ Imports NameTy ->
+ ModulesTy src -> src -> Len vs -> Mod NameTy ->
  Either (Error_Type src) (TypeT src vs)
-readTyName cs src len name =
-	case Map.lookup name cs of
+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
 
@@ -75,47 +79,12 @@
 readVars evs (BinTree2 x y) =
 	readVars (readVars evs x) y
 
--- * Type 'Name2Type'
-type Name2Type src = Map NameTy (TypeTLen src)
-
--- ** Type 'TypeTLen'
--- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
---
--- Useful to build a 'Name2Type' which can be used
--- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
-newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
-instance Source src => Eq (TypeTLen src) where
-	TypeTLen x == TypeTLen y = x LenZ == y LenZ
-instance Source src => Show (TypeTLen src) where
-	showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
-
--- ** Class 'Inj_Name2Type'
--- | Derive a 'Name2Type' from the given type-level list
--- of 'Proxy'-fied /type constants/.
-class Inj_Name2Type cs where
-	inj_Name2Type :: Source src => Name2Type src
-instance Inj_Name2Type '[] where
-	inj_Name2Type = Map.empty
-instance
- ( Inj_KindP (Ty_of_Type (K c))
- , K c ~ Type_of_Ty (Ty_of_Type (K c))
- , Constable c
- , Inj_Name2Type cs
- ) => Inj_Name2Type (Proxy c ': cs) where
-	inj_Name2Type =
-		Map.insert
-		 (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
-		 (TypeTLen $ \len -> TypeT $ TyConst noSource len $
-			inj_ConstKi @(K c) @c $
-			inj_KindP @(Ty_of_Type (K c)) noSource) $
-		inj_Name2Type @cs
-
 -- * Type 'Error_Type'
 data Error_Type src
- =   Error_Type_Constant_unknown (At src NameTy)
+ =   Error_Type_Constant_unknown (At src (Mod NameTy))
  |   Error_Type_Con_Kind         (Con_Kind src)
  deriving (Eq, Show)
-instance Inj_Error (Error_Type src) (Error_Type src) where
-	inj_Error = id
-instance Inj_Error (Con_Kind src) (Error_Type src) where
-	inj_Error = Error_Type_Con_Kind
+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/Show.hs b/Language/Symantic/Typing/Show.hs
--- a/Language/Symantic/Typing/Show.hs
+++ b/Language/Symantic/Typing/Show.hs
@@ -2,29 +2,32 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Typing.Show where
 
-import Data.Semigroup ((<>))
 import qualified Data.Text.Lazy as TL
 import qualified Data.Text.Lazy.Builder as TLB
 
 import qualified Language.Symantic.Document as D
 import Language.Symantic.Grammar
 import Language.Symantic.Typing.Type
+import Language.Symantic.Typing.Module
 import Language.Symantic.Typing.Document
 
 showType :: Config_Doc_Type -> Type src vs t -> String
 showType conf ty = TL.unpack $ TLB.toLazyText $ D.plain $ docType conf 0 ty
 
 showTypeS :: Config_Doc_Type -> Precedence -> Type src vs t -> ShowS
-showTypeS conf pr ty s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty)
+showTypeS conf pr ty = showString $ TL.unpack (TLB.toLazyText $ D.plain $ docType conf pr ty)
 
 showTypes :: Config_Doc_Type -> Types src vs ts -> String
 showTypes conf tys = TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)
 
 showTypesS :: Config_Doc_Type -> Types src vs ts -> ShowS
-showTypesS conf tys s = s <> TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)
+showTypesS conf tys = showString $ TL.unpack (TLB.toLazyText $ D.plain $ docTypes conf tys)
 
+instance NameTyOf c => Show (Const src c) where
+	showsPrec _p = showString . TL.unpack . TLB.toLazyText . D.plain . docConst mempty
+
 instance Source src => Show (Type src vs t) where
-	showsPrec = showTypeS config_doc_type
+	showsPrec = showTypeS config_Doc_Type
 instance Source src => Show (TypeK src vs kt) where
 	showsPrec p (TypeK t) = showsPrec p t
 instance Source src => Show (TypeVT src) where
@@ -32,4 +35,4 @@
 instance Source src => Show (TypeT src vs) where
 	showsPrec p (TypeT t) = showsPrec p t
 instance Source src => Show (Types src vs ts) where
-	showsPrec _ = showTypesS config_doc_type
+	showsPrec _ = showTypesS config_Doc_Type
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,12 +1,8 @@
 {-# language ConstraintKinds #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# LANGUAGE ImpredicativeTypes #-}
-{-# LANGUAGE LiberalTypeSynonyms #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -32,6 +28,7 @@
 import Language.Symantic.Typing.List
 import Language.Symantic.Typing.Kind
 import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.Module
 
 -- * Type 'Type'
 data Type (src::K.Type) (vs::[K.Type]) (t::kt) where
@@ -64,7 +61,7 @@
 
 instance Source src => Eq (Type src vs t) where
 	x == y = isJust $ eqType x y
-instance Inj_Source (TypeVT src) src => TestEquality (Type src vs) where
+instance SourceInj (TypeVT src) src => TestEquality (Type src vs) where
 	testEquality = eqType
 
 type instance SourceOf (Type src vs t) = src
@@ -79,8 +76,8 @@
 	setSource (TyVar   _src n v)    src = TyVar   src n v
 	setSource (TyFam   _src l f as) src = TyFam   src l f as
 
-instance Inj_Source (TypeVT src) src => KindOf (Type src vs) where
-	kindOf t = kindOfType t `source` TypeVT t
+instance SourceInj (TypeVT src) src => KindOf (Type src vs) where
+	kindOf t = kindOfType t `withSource` TypeVT t
 
 instance ConstsOf (Type src vs t) where
 	constsOf (TyConst _src _len c)    = Set.singleton $ ConstC c
@@ -121,33 +118,31 @@
 	allocVarsR len (TyVar src n v)    = TyVar src n $ allocVarsR len v
 	allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as
 
--- | Like 'TyConst', but using 'noSource' and 'inj_Const'.
+-- | Like 'TyConst', but using 'noSource', 'lenInj' and 'constInj'.
 -- 
 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
 tyConst ::
  forall kc (c::kc) src vs.
  Source src =>
- Inj_Len vs =>
+ LenInj vs =>
  Constable c =>
- Inj_KindP (Ty_of_Type kc) =>
+ KindInjP (Ty_of_Type kc) =>
  Type_of_Ty (Ty_of_Type kc) ~ kc =>
  Type src vs c
-tyConst = TyConst noSource inj_Len inj_Const
+tyConst = TyConst noSource lenInj constInj
  -- NOTE: The forall brings @c@ first in the type variables,
  -- which is convenient to use @TypeApplications@.
 
--- | Like 'TyConst', but using 'noSource' and 'inj_Const'.
--- 
--- FIXME: remove @kc@ when GHC's #12933 is fixed.
+-- | Like 'tyConst', but not using 'lenInj'.
 tyConstLen ::
  forall kc (c::kc) src vs.
  Source src =>
  Constable c =>
- Inj_KindP (Ty_of_Type kc) =>
+ KindInjP (Ty_of_Type kc) =>
  Type_of_Ty (Ty_of_Type kc) ~ kc =>
  Len vs ->
  Type src vs c
-tyConstLen len = TyConst noSource len inj_Const
+tyConstLen len = TyConst noSource len constInj
 
 -- | Like 'TyApp', but using 'noSource'.
 tyApp ::
@@ -172,13 +167,13 @@
 tyFam ::
  forall kc (c::kc) as vs src.
  Source src =>
- Inj_Len vs =>
+ LenInj vs =>
  Constable c =>
- Inj_KindP (Ty_of_Type kc) =>
+ KindInjP (Ty_of_Type kc) =>
  Type_of_Ty (Ty_of_Type kc) ~ kc =>
  Types src vs as ->
  Type src vs (Fam c as)
-tyFam = TyFam noSource inj_Len (inj_Const @c)
+tyFam = TyFam noSource lenInj (constInj @c)
 
 -- | Qualify a 'Type'.
 tyQual ::
@@ -223,15 +218,13 @@
 -- * Type 'Const'
 -- | /Type constant/.
 data Const src (c::kc) where
-	Const :: Constable c
-	      => Kind src kc
-	      -> Const src (c::kc)
+	Const :: Constable c => Kind src kc -> Const src (c::kc)
 
 type instance SourceOf (Const src c) = src
 instance ConstsOf (Const src c) where
 	constsOf = Set.singleton . ConstC
-instance Inj_Source (ConstC src) src => KindOf (Const src) where
-	kindOf c@(Const kc) = kc `source` ConstC c
+instance SourceInj (ConstC src) src => KindOf (Const src) where
+	kindOf c@(Const kc) = kc `withSource` ConstC c
 
 kindOfConst :: Const src (t::kt) -> Kind src kt
 kindOfConst (Const kc) = kc
@@ -240,12 +233,14 @@
 class
  ( Typeable c
  , FixityOf c
+ , NameTyOf c
  , ClassInstancesFor c
  , TypeInstancesFor c
  ) => Constable c
 instance
  ( Typeable c
  , FixityOf c
+ , NameTyOf c
  , ClassInstancesFor c
  , TypeInstancesFor c
  ) => Constable c
@@ -255,18 +250,6 @@
 class ConstsOf a where
 	constsOf :: a -> Set (ConstC (SourceOf a))
 
--- ** Class 'FixityOf'
--- | Return the 'Fixity' of something.
-class FixityOf (c::kc) where
-	fixityOf :: proxy c -> Maybe Fixity
-	fixityOf _c = Nothing
-instance FixityOf (c::K.Type)
-instance FixityOf (c::K.Constraint)
-
--- Show
-instance Show (Const src c) where
-	showsPrec p c@Const{} = showsPrec p $ typeRep c
-
 -- ** Type 'ConstC'
 data ConstC src
  = forall c. ConstC (Const src c)
@@ -307,7 +290,7 @@
 -- the argument of that function.
 unTyFun ::
  forall t src tys.
- Inj_Source (TypeVT src) src =>
+ SourceInj (TypeVT src) src =>
  Constable (->) =>
  Type src tys t ->
  Maybe ( Type src tys (FunArg t)
@@ -320,7 +303,7 @@
 	       , Type src tys (FunRes x) )
 	go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 	 | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
-	 = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini))
+	 = Just ((a `withSource` TypeVT ty_ini), (b `withSource` TypeVT ty_ini))
 	go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 	 = go b
@@ -332,17 +315,20 @@
 -- ** Type @(#>)@
 -- | /Type constant/ to qualify a 'Type'.
 newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)
+instance NameTyOf (#>) where
+	nameTyOf _c = [] `Mod` "=>"
 instance FixityOf (#>) where
 	fixityOf _c = Just $ Fixity2 $ infixR 0
 instance ClassInstancesFor (#>)
 instance TypeInstancesFor  (#>)
 
+-- | Qualify a 'Type'.
 (#>) ::
  Source src =>
- Type src vs a ->
- Type src vs b ->
- Type src vs (a #> b)
-(#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b
+ Type src vs q ->
+ Type src vs t ->
+ Type src vs (q #> t)
+(#>) q t = (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 infixr 0 #>
  -- NOTE: should actually be (-1)
  -- to compose well with @infixr 0 (->)@
@@ -352,6 +338,8 @@
 -- | 'K.Constraint' union.
 class    (x, y) => x # y
 instance (x, y) => x # y
+instance NameTyOf (#) where
+	nameTyOf _c = [] `Mod` ","
 instance FixityOf (#) where
 	fixityOf _c = Just $ Fixity2 $ infixB SideL 0
 instance ClassInstancesFor (#) where
@@ -363,6 +351,7 @@
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (#)
 
+-- | Unify two 'K.Constraint's.
 (#) ::
  Source src =>
  Type src vs qx ->
@@ -371,18 +360,10 @@
 (#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 infixr 2 #
 
-noConstraint ::
- Source src =>
- Inj_Len vs =>
- Type src vs (()::K.Constraint)
-noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) inj_Len
-
-noConstraintLen ::
- Source src =>
- Len vs ->
- Type src vs (()::K.Constraint)
-noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)
-
+-- ** Type @(() :: @'K.Constraint'@)@
+instance NameTyOf (()::K.Constraint) where
+	nameTyOf _c = [] `Mod` "()"
+-- instance FixityOf (()::Constraint)
 instance ClassInstancesFor (()::K.Constraint) where
 	proveConstraintFor _c q
 	 | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q
@@ -390,14 +371,25 @@
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (()::K.Constraint)
 
+-- | Like 'noConstraintLen', but using 'lenInj'.
+noConstraint :: Source src => LenInj vs => Type src vs (()::K.Constraint)
+noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) lenInj
+
+-- | Empty 'K.Constraint'.
+noConstraintLen :: Source src => Len vs -> Type src vs (()::K.Constraint)
+noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)
+
 -- ** Class @(#~)@
 -- | /Type equality/ 'K.Constraint'.
 class    (x ~ y) => x #~ y
 instance (x ~ y) => x #~ y
+instance NameTyOf (#~) where
+	nameTyOf _c = [] `Mod` "~"
+	isNameTyOp _c = True
 instance FixityOf (#~) where
 	fixityOf _ = Just $ Fixity2 $ infixB SideL 0
 instance
- ( Inj_Kind k
+ ( KindInj k
  , Typeable k
  ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where
 	proveConstraintFor _c (TyApp _ (TyApp _ c a) b)
@@ -407,27 +399,18 @@
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor  (#~)
 
+-- | Constraint two 'Type's to be equal.
 (#~) ::
  forall k a b src vs.
  Source src =>
  Typeable k =>
- Inj_Kind k =>
+ KindInj k =>
  Type src vs (a :: k) ->
  Type src vs (b :: k) ->
  Type src vs (a #~ b)
 (#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b
 infixr 2 #~
 
-{-
-const_EqTy ::
- forall k src.
- Source src =>
- Typeable k =>
- Inj_Kind k =>
- Const src ((#~)::k -> k -> K.Constraint)
-const_EqTy = inj_Const @(#~)
--}
-
 -- | /Type equality/.
 eqType ::
  Source src =>
@@ -525,22 +508,22 @@
 	where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)
 
 -- ** Injection
-inj_Const ::
+constInj ::
  forall c src.
  Source src =>
  Constable c =>
- Inj_KindP (Ty_of_Type (K c)) =>
+ KindInjP (Ty_of_Type (K c)) =>
  Type_of_Ty (Ty_of_Type (K c)) ~ K c =>
  Const src c
-inj_Const = Const $ inj_KindP @(Ty_of_Type (K c)) noSource
+constInj = Const $ kindInjP @(Ty_of_Type (K c)) noSource
 
-inj_ConstKi ::
+constKiInj ::
  forall kc c src.
  Source src =>
  Constable c =>
  Kind src kc ->
  Const src (c::kc)
-inj_ConstKi = Const
+constKiInj = Const
 
 -- ** Projection
 {- XXX: not working because of GHC's #12933
@@ -548,11 +531,11 @@
  forall c u src.
  Constable c =>
  (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>
- Inj_Kind (K c) =>
+ KindInj (K c) =>
  Const src u ->
  Maybe (c :~~: u)
 proj_ConstKi (Const ku) = do
-	Refl <- eqKind ku $ inj_Kind @(K c) @()
+	Refl <- eqKind ku $ kindInj @(K c) @()
 	Refl :: u:~:c <- eqT
 	Just HRefl
 -}
@@ -581,11 +564,11 @@
  forall kc (c::kc) u src.
  Typeable c =>
  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
- Inj_KindP (Ty_of_Type kc) =>
+ KindInjP (Ty_of_Type kc) =>
  Const src u ->
  Maybe (c :~~: u)
 proj_ConstKi (Const ku) = do
-	Refl <- eqKind ku $ inj_KindP @(Ty_of_Type kc) ()
+	Refl <- eqKind ku $ kindInjP @(Ty_of_Type kc) ()
 	Refl :: u:~:c <- eqT
 	Just HRefl
 
@@ -594,7 +577,7 @@
  forall kc (c::kc) u src vs.
  Typeable c =>
  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
- Inj_KindP (Ty_of_Type kc) =>
+ KindInjP (Ty_of_Type kc) =>
  Type src vs u ->
  Maybe (c :~~: u)
 proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c
@@ -666,11 +649,11 @@
 		 (Nothing, Nothing) ->
 			case q0' `ordType` q1' of
 			 LT ->
-				let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in
+				let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ constInj @(#)) q0') q1' in
 				TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t
 			 EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t
 			 GT ->
-				let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in
+				let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ constInj @(#)) q1') q0' in
 				TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t
 	-- q => t
 	go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
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
@@ -130,10 +130,10 @@
 deriving instance Source src => Eq   (Error_Unify src)
 deriving instance Source src => Show (Error_Unify src)
 
-instance Inj_Error (Error_Unify src) (Error_Unify src) where
-	inj_Error = id
-instance Inj_Error (Con_Kind src) (Error_Unify src) where
-	inj_Error = Error_Unify_Kind
+instance ErrorInj (Error_Unify src) (Error_Unify src) where
+	errorInj = id
+instance ErrorInj (Con_Kind src) (Error_Unify src) where
+	errorInj = Error_Unify_Kind
 
 -- | Return the left spine of a 'Type':
 -- the root 'Type' and its 'Type' parameters,
@@ -141,7 +141,7 @@
 spineTy ::
  forall src vs t.
  Source src =>
- Inj_Source (TypeVT src) src =>
+ SourceInj (TypeVT src) src =>
  Type src vs t ->
  (TypeT src vs, [TypeT src vs])
 spineTy typ = go [] typ
@@ -150,8 +150,8 @@
 	go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
 	 | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
 	 = go ctx t -- NOTE: skip the constraint @q@.
-	go ctx (TyApp  _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f
-	go ctx t = (TypeT (t `source` TypeVT typ), ctx)
+	go ctx (TyApp  _src f a) = go (TypeT (a `withSource` TypeVT typ) : ctx) f
+	go ctx t = (TypeT (t `withSource` TypeVT typ), ctx)
 
 {-
 spineTy
@@ -173,8 +173,8 @@
 -- | Return the /most general unification/ of two 'Type's, when it exists.
 unifyType ::
  forall ki (x::ki) (y::ki) vs src.
- Inj_Source (TypeVT src) src =>
- Inj_Error (Con_Kind src) (Error_Unify src) =>
+ SourceInj (TypeVT src) src =>
+ ErrorInj (Con_Kind src) (Error_Unify src) =>
  Subst src vs ->
  Type src vs (x::ki) ->
  Type src vs (y::ki) ->
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
@@ -34,8 +34,8 @@
 type instance SourceOf (Var src vs t) = src
 instance Show (Var src tys v) where
 	showsPrec p v = showsPrec p (indexVar v)
-instance Inj_Source (EVar src vs) src => KindOf (Var src vs) where
-	kindOf v = kindOfVar v `source` EVar v
+instance SourceInj (EVar src vs) src => KindOf (Var src vs) where
+	kindOf v = kindOfVar v `withSource` EVar v
 instance LenVars (Var src vs v) where
 	lenVars (VarZ _k l) = l
 	lenVars (VarS v)    = LenS (lenVars v)
@@ -49,10 +49,10 @@
 varZ ::
  forall src vs kv (v::kv).
  Source src =>
- Inj_Len vs =>
- Inj_Kind kv =>
+ LenInj vs =>
+ KindInj kv =>
  Var src (Proxy v ': vs) v
-varZ = VarZ inj_Kind inj_Len
+varZ = VarZ kindInj lenInj
 
 -- | Return the 'Kind' of given 'Var'.
 kindOfVar :: Var src vs (v::kv) -> Kind src kv
diff --git a/symantic.cabal b/symantic.cabal
--- a/symantic.cabal
+++ b/symantic.cabal
@@ -3,216 +3,10 @@
 build-type: Simple
 cabal-version: >= 1.24
 category: Language
-description:
- __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:
- .
- * /first class functions/ (aka. /lambdas/),
- * chosen /monomorphic types/ (like 'Bool' or 'Maybe'),
- * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@),
- * chosen /type class instances/,
- * chosen /type family instances/,
- * and chosen /type constraints/;
- .
- where "chosen X" means declared in Haskell
- and selected when composing the DSL.
- .
- In particular, this library is currently not able to:
- .
- * do /type inferencing/ for the argument of /lambdas/
-   (they must all be explicitely annotated, aka. /Church-style/),
- * do /pattern matching/ (aka. /case/) (but /Church-encoding/ functions are often enough),
- * do /rank-N polymorphic types/ (aka. /non-prenex forall/, like @(forall s. ST s a) -> a@).
- .
- And by itself, the DSL is only able to define new terms to be interpreted,
- no new types, or other type-level structures.
- .
- __Warning__
- .
- Please be aware that despite its using of powerful ideas from clever people,
- this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY.
- Meaning that it IS NOT heavily tested and documented,
- DOES NOT have a strong commitment to preserving backward compatibility,
- MAY FAIL to comply with the <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,
- and CAN die without notice.
- You've been warned.
- .
- __Use cases__
- .
- The main goal of this library is to enable the runtime interpretation of terms,
- type-checked according to some types defined at composing-time (ie. GHC's compile-time).
- .
- Using a DSL enables to limit expressiveness in order to ease analysis.
- Here the idea is that the more complex logic shall remain written in Haskell,
- and then this library used to project an interface into a DSL
- (using GHC's Haskell as a FFI (Foreign Function Interface)).
- This in order to give runtime users the flexibility
- to write programs not requiring a full-blown Haskell compiler,
- yet enabling enough flexibility to let them express complex needs
- with a reasonably advanced type-safe way
- and a controlled environment of primitives.
- .
- Typical use cases:
- .
- * Enabling runtime users to enter some Haskell-like expressions
-   (maybe with a more convenient syntax wrt. the domain problem)
-   without using at runtime all the heavy machinery and ecosystem of GHC
-   (eg. by using <https://hackage.haskell.org/package/hint hint>),
-   but still leaning on primitive functions coded in GHC's Haskell.
- * Limiting those expressions to be built from well-controlled expressions only.
- * Run some analyzes/optimizations on those well-controlled expressions.
- .
- __Usage__
- .
- Please pick in <https://hackage.haskell.org/package/symantic-lib 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://git.autogeree.net/symantic Git repository>,
- to learn by examples how to use this library.
- .
- Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
- (see @Grammar/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
- with <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —
- can be reused to build other ones, is not bound to a specific parser,
- and can produce its own EBNF rendition.
- .
- __Acknowledgements__
- .
- This library would probably be much worse than it is
- without the following seminal works:
- .
- * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
- * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.
- .
- __Main ideas__
- .
- * __Symantic DSL__.
-   Terms are encoded in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way (aka. the /symantic/ way)
-   which leverages the /type class/ system of Haskell — instead of using /data types/ — to form an embedded DSL.
-   More specifically, a /class/ encodes the /syntax/ of terms (eg. 'Sym_Bool')
-   and its /class instances/ on a dedicated type encodes their /semantics/
-   (eg. @(Sym_Bool Eval)@ interprets a term as a value of its type
-   in the host language ('Bool' in Haskell here),
-   or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.).
-   
-   DSL are then composed/extended by selecting those symantic /classes/
-   (and in an embedded DSL those could even be automatically inferred,
-   when @NoMonomorphismRestriction@ is on).
-   Otherwise, when using symantics for a non-embedded DSL
-   — the whole point of this library — the /classes/ composing the DSL
-   are selected manually at GHC's compile-time,
-   through the /type-level list/ @ss@ given to 'readTerm'.
-   
-   Moreover, those symantic @term@s are parameterized by the type of the value they encode,
-   in order to get the same type safety as with plain Haskell values.
-   Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@
-   instead of just @(* -> Constraint)@.
-   
-   Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,
-   meaning that they directly reuse GHC's internal machinery
-   to abstract or instantiate variables,
-   which I think is by far the most efficient and simplest way of doing it
-   (no (generalized or not) DeBruijn encoding
-   like in <https://hackage.haskell.org/package/bound bound>'s @Monad@s).
- 
- * __Singleton for any type__.
-   To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/
-   for any Haskell /type index/ @t@ of any kind,
-   which is made possible with the dependant Haskell extensions:
-   especially @TypeFamilies@, @GADTs@ and @TypeInType@.
- 
- * __Type constants using 'Typeable'__.
-   /Type constant/ could be introduced by indexing them amongst a /type-level list/,
-   but since they are /monomorphic types/, using 'Typeable' simplifies
-   the machinery, and is likely more space/time efficient, including at GHC-compile-time.
- 
- * __Type variables using a type-level list__.
-   Handling /type variables/ is done by indexing them amongst a @vs@ /type-level list/,
-   where each /type variable/ is wrapped inside a @Proxy@ to handle different kinds.
-   Performing a substitution (in 'substVar') preserves the /type index/ @t@,
-   which is key for preserving any associated 'Term'.
-   Unifying /type variables/ is done with 'unsafeCoerce' (in 'unifyType'),
-   which I think is necessary and likely safe.
- 
- -- NOTE: no longer used.
- -- * __Extensible data type__.
- --   To inject a type into a /type-level list/
- --   or project a /type-level list/ onto a type,
- --   to compose an /extensible data type/
- --   (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
- --   that a parser can build and then give to 'compile').
- --   This type-level programming requires @UndecidableInstances@,
- --   but not @OverlappingInstances@.
- -- 
- --   There is a similarity with
- --   <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
- --   (see for instance <https://hackage.haskell.org/package/compdata compdata>
- --   or <https://hackage.haskell.org/package/syntactic syntactic>).
- --   Those also enable to compose a DSL using some machinery
- --   based upon (co)free(r) (co)monads and (cata|ana)morphisms.
- --   Which library fits best your problem domain and brain is for you to judge :)
- --   On that topic, see also:
- --   <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
- --
- -- Here, I just came up using /type-level lists/ by hacking
- -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
- .
- __Main extensions__
- .
- * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.
- * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,
-   or reifying any 'Constraint' as an explicit dictionary 'Dict',
-   or defining /type synonym/ of /type classes/,
-   or merging /type constraints/.
- * @DataKinds@ for type-level data structures (eg. /type-level lists/).
- * @DefaultSignatures@ for providing identity transformations of terms,
-   and thus avoid boilerplate code when a transformation
-   does not need to alter all semantics.
-   Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
- * @GADTs@ for knowing types by pattern-matching terms,
-   or building terms by using type classes.
- * @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).
- * @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.
-   Which makes the /type application/ ('TyApp')
-   give us an /arrow kind/ for the Haskell /type constructor/
-   it applies an Haskell type to, releaving me from tricky workarounds.
- * @UndecidableInstances@ for type-level programming that may never terminate.
- .
- __Bugs__
- .
- There are some of them hidding in there,
- and the whole thing is far from being perfect…
- Your comments, problem reports, or questions, are welcome!
- You have my email address, so… just send me some emails :]
- .
- __To do__
- .
- * Study to which point /type inferencing/ is doable,
-   now that 'Type' is powerful enough to contain 'TyVar's.
- * Study to which point error messages can be improved,
-   now that there is a 'Source' carried through all 'Kind's or 'Type's,
-   it should enable some nice reports.
-   Still, a lot of work and testing remain to be done,
-   and likely some ideas to find too…
- * Add more terms in <https://hackage.haskell.org/package/symantic-lib symantic-lib>.
- * Add more transformations.
- * Study how to integrate types into the module system.
- * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
- * Study how to support /rank-N polymorphic types/,
-   special cases can likely use the /boxed polymorphism/ workaround,
-   but even if GHC were supporting /impredicative types/,
-   I'm currently clueless about how to do this.
+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-source-files:
 extra-tmp-files:
 -- homepage: 
@@ -226,7 +20,7 @@
 -- PVP:  +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 6.0.0.20170623
+version: 6.2.0.20170702
 
 Source-Repository head
   location: git://git.autogeree.net/symantic
@@ -272,6 +66,7 @@
     Language.Symantic.Typing.Grammar
     Language.Symantic.Typing.Kind
     Language.Symantic.Typing.List
+    Language.Symantic.Typing.Module
     Language.Symantic.Typing.Peano
     Language.Symantic.Typing.Read
     Language.Symantic.Typing.Show