diff --git a/Language/Symantic/Compiling/Test.hs b/Language/Symantic/Compiling/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Compiling/Test.hs
+++ /dev/null
@@ -1,112 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Compiling.Test where
-
-import Test.Tasty
-import Test.Tasty.HUnit
-import Debug.Trace (trace)
-
-import Control.Arrow (left)
-import Data.Functor.Identity (Identity(..))
-import Data.Text (Text)
-import Data.Type.Equality
-import qualified Control.Monad.Classes.Run as MC
-import qualified Control.Monad.Trans.State.Strict as SS
-import qualified Data.List as List
-import qualified Data.Text as Text
-import qualified Text.Megaparsec as P
-
-import Language.Symantic.Grammar
-import Language.Symantic
-import Language.Symantic.Lib ()
-
-import Grammar.Megaparsec ()
-
-type G src ss =
- P.ParsecT P.Dec Text
-           (SS.StateT (Imports NameTe, Modules src ss)
-                      ((SS.StateT (Imports NameTy, ModulesTy src))
-                                  Identity))
-
-parseTe ::
- forall ss src.
- ImportTypes ss =>
- ModulesTyInj ss =>
- ModulesInj src ss =>
- Gram_Term src ss (G src ss) =>
- Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
-parseTe inp =
-	let modsTe :: Modules src ss = either (error . show) id modulesInj in
-	let impsTe = [] `importModules` modsTe in
-	let modsTy = modulesTyInj @ss @src in
-	let impsTy = importTypes @ss [] in
-	runIdentity $
-	MC.evalStateStrict (impsTy, modsTy) $
-	MC.evalStateStrict (impsTe, modsTe) $
-	P.runParserT g "" inp
-	where g = unCF $ g_term <* eoi
-
-readTe ::
- forall src ss t.
- ( Eq t
- , Eq src
- , Gram_Term src ss (G src ss)
- , ImportTypes ss
- , ModulesInj src ss
- , ModulesTyInj ss
- , Show src
- , Show t
- , SourceInj (AST_Type src) src
- , SourceInj (KindK src) src
- , SourceInj (TypeT src '[]) src
- , SourceInj (TypeVT src) src
- , Syms ss (BetaT View)
- , Syms ss Eval
- , Syms ss View
- ) =>
- Text ->
- Either ( Type src '[] t
-        , Either (P.ParseError Char P.Dec)
-                 (Error_Term src) )
-        (Type src '[] t, t, Text) ->
- TestTree
-readTe inp expected =
-	testCase (elide inp) $
-	case reduceTeApp <$> parseTe @ss inp of
-	 Left err -> Left (Left err) @?= snd `left` expected
-	 Right ast ->
-		case readTerm CtxTyZ ast of
-		 Left err -> Left (Right err) @?= snd `left` expected
-		 Right term ->
-			case term of
-			 TermVT (Term q t (TeSym te)) ->
-				case expected of
-				 Left (_, err) -> Right ("…"::Text) @?= Left err
-				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->
-					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
-					case lenVars t of
-					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
-					 LenZ ->
-						case proveConstraint q of
-						 Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
-						 Just Dict ->
-							case t `eqType` ty_expected of
-							 Nothing -> return $ Left $ Right $
-								Error_Term_Beta $ Error_Beta_Unify $
-								Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
-							 Just Refl ->
-								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
-
-maybeRight :: Either l r -> Maybe r
-maybeRight (Right r) = Just r
-maybeRight Left{}    = Nothing
-
-elide :: Text -> String
-elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
-elide s = Text.unpack s
-
-dbg :: Show a => String -> a -> a
-dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x
diff --git a/Language/Symantic/Grammar/EBNF.hs b/Language/Symantic/Grammar/EBNF.hs
deleted file mode 100644
--- a/Language/Symantic/Grammar/EBNF.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-module Grammar.EBNF where
-
-import Data.Text.IO as Text
-import Control.Monad
-
-import Language.Symantic.Grammar
-import Language.Symantic
-import Language.Symantic.Lib ()
-
-main :: IO ()
-main = do
-	forM_ gram_comment render
-	forM_ gram_type render
-	forM_ gram_term render
-	where render = Text.putStrLn . renderEBNF . unCF
diff --git a/Language/Symantic/Grammar/Megaparsec.hs b/Language/Symantic/Grammar/Megaparsec.hs
deleted file mode 100644
--- a/Language/Symantic/Grammar/Megaparsec.hs
+++ /dev/null
@@ -1,167 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
--- | Symantic instances for Megaparsec
-module Grammar.Megaparsec where
-
-import Control.Applicative (Applicative(..))
-import Control.Monad (Monad(..))
-import Data.Char (Char)
-import Data.Either (Either(..))
-import Data.Function (($), (.))
-import Data.Functor (Functor(..), (<$>))
-import Data.List.NonEmpty (NonEmpty(..))
-import Data.Ord (Ord(..))
-import Data.String (IsString(..))
-import Data.Typeable ()
-import Text.Show (Show(..))
-import qualified Control.Applicative as Alt
-import qualified Control.Monad.Classes as MC
-import qualified Data.Char as Char
-import qualified Data.Text as Text
-import qualified Text.Megaparsec as P
-
-import Language.Symantic.Grammar as Sym
-import qualified Language.Symantic as Sym
-import Language.Symantic.Lib ()
-
--- * Type 'ParsecC'
--- | Convenient alias for defining instances involving 'P.ParsecT'.
-type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)
-instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where
-	fromString = P.string
-
---
--- Readers
---
-
--- NonEmpty P.SourcePos
-instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where
-	askBefore g = do
-		s <- P.statePos <$> P.getParserState
-		($ s) <$> g
-	askAfter g = do
-		f <- g
-		f . P.statePos <$> P.getParserState
-type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True
-instance ParsecC e s => MC.MonadReaderN 'MC.Zero (NonEmpty P.SourcePos) (P.ParsecT e s m) where
-	askN _n = P.statePos <$> P.getParserState
--- P.SourcePos
-instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where
-	askBefore g = do
-		s <- P.getPosition
-		($ s) <$> g
-	askAfter g = do
-		f <- g
-		f <$> P.getPosition
-type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True
-instance ParsecC e s => MC.MonadReaderN 'MC.Zero P.SourcePos (P.ParsecT e s m) where
-	askN _n = P.getPosition
--- ()
-instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where
-	askBefore = fmap ($ ())
-	askAfter  = fmap ($ ())
-
---
--- States
---
-
--- st
-type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False
-instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where
-	stateBefore g = do
-		s <- MC.get
-		f <- g
-		let (s', a) = f s
-		MC.put s'
-		return a
-	stateAfter g = do
-		f <- g
-		s <- MC.get
-		let (s_, a) = f s
-		MC.put s_
-		return a
-	getBefore g = do
-		s <- MC.get
-		f <- g
-		return (f s)
-	getAfter g = do
-		f <- g
-		s <- MC.get
-		return (f s)
-	put g = do
-		(s, a) <- g
-		MC.put s
-		return a
-
---
--- Sym instances
---
-instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where
-	catch me {- if you can :-} = do
-		e <- me
-		case e of
-		 Left err -> fail $ show err
-		 Right a -> return a
-instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where
-	rule = P.label . Text.unpack
-instance ParsecC e s => Sym.Gram_Terminal (P.ParsecT e s m) where
-	any          = P.anyChar
-	eoi          = P.eof
-	char         = P.char
-	string       = P.string
-	unicat cat   = P.satisfy $ (`elem` cats) . Char.generalCategory
-		where cats = unicode_categories cat
-	range (l, h) = P.satisfy $ \c -> l <= c && c <= h
-	Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f
-instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where
-	empty  = Alt.empty
-	(<+>)  = (Alt.<|>)
-	choice = P.choice
-instance ParsecC e s => Sym.Gram_Try (P.ParsecT e s m) where
-	try = P.try
-instance ParsecC e s => Sym.Gram_RegR (P.ParsecT e s m) where
-	Terminal f .*> Reg x = Reg $ f <*> x
-instance ParsecC e s => Sym.Gram_RegL (P.ParsecT e s m) where
-	Reg f <*. Terminal x = Reg $ f <*> x
-instance ParsecC e s => Sym.Gram_App (P.ParsecT e s m) where
-	between = P.between
-instance ParsecC e s => Sym.Gram_AltApp (P.ParsecT e s m) where
-	option   = P.option
-	optional = P.optional
-	many     = P.many
-	some     = P.some
-	skipMany = P.skipMany
-instance ParsecC e s => Sym.Gram_CF (P.ParsecT e s m) where
-	CF f <& Reg p        = CF $ P.lookAhead f <*> p
-	Reg f &> CF p        = CF $ P.lookAhead f <*> p
-	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f
-instance ParsecC e s => Sym.Gram_Comment (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Op (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Mod (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Type_Name (P.ParsecT e s m)
-instance ParsecC e s => Sym.Gram_Term_Name (P.ParsecT e s m)
-instance -- Sym.Gram_Type
- ( ParsecC e s
- , Gram_Source src (P.ParsecT e s m)
- , Show src
- , MC.MonadState ( Sym.Imports Sym.NameTy
-                 , Sym.ModulesTy src ) (P.ParsecT e s m)
- ) => Sym.Gram_Type src (P.ParsecT e s m)
-instance -- Sym.Gram_Term_Type
- ( ParsecC e s
- , Show src
- , MC.MonadState ( Sym.Imports Sym.NameTy
-                 , Sym.ModulesTy src ) (P.ParsecT e s m)
- , Gram_Source src           (P.ParsecT e s m)
- ) => Sym.Gram_Term_Type src (P.ParsecT e s m)
-instance -- Sym.Gram_Term
- ( ParsecC e s
- , Show src
- , MC.MonadState ( Sym.Imports Sym.NameTy
-                 , Sym.ModulesTy src )  (P.ParsecT e s m)
- , MC.MonadState ( Sym.Imports Sym.NameTe
-                 , Sym.Modules src ss ) (P.ParsecT e s m)
- , Sym.Gram_Source src        (P.ParsecT e s m)
- , Sym.Gram_Term_Atoms src ss (P.ParsecT e s m)
- ) => Sym.Gram_Term src ss    (P.ParsecT e s m)
diff --git a/Language/Symantic/Lib/Alternative.hs b/Language/Symantic/Lib/Alternative.hs
--- a/Language/Symantic/Lib/Alternative.hs
+++ b/Language/Symantic/Lib/Alternative.hs
@@ -4,7 +4,7 @@
 module Language.Symantic.Lib.Alternative where
 
 import Control.Applicative (Alternative)
-import Prelude hiding (Functor(..), (<$>), id, const)
+import Prelude hiding (Functor(..))
 import qualified Control.Applicative as Alternative
 
 import Language.Symantic
diff --git a/Language/Symantic/Lib/Applicative.hs b/Language/Symantic/Lib/Applicative.hs
--- a/Language/Symantic/Lib/Applicative.hs
+++ b/Language/Symantic/Lib/Applicative.hs
@@ -4,7 +4,7 @@
 module Language.Symantic.Lib.Applicative where
 
 import Control.Applicative (Applicative)
-import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)
+import Prelude hiding (Functor(..), (<$>), Applicative(..))
 import qualified Control.Applicative as Applicative
 import qualified Data.Function as Fun
 
diff --git a/Language/Symantic/Lib/Applicative/Test.hs b/Language/Symantic/Lib/Applicative/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Applicative/Test.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Applicative.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
-
-import Language.Symantic.Lib
-import Compiling.Test
-import Lib.Bool.Test ()
-
-type SS =
- [ Proxy (->)
- , Proxy Integer
- , Proxy Bool
- , Proxy Maybe
- , Proxy Functor
- , Proxy Applicative
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Applicative"
- [ "Just (xor True) <*> Just True"    ==> Right (tyMaybe tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True")
- , "Just (xor True) <*> Nothing"      ==> Right (tyMaybe tyBool, Nothing   , "Just (\\x0 -> True `xor` x0) <*> Nothing")
- , "xor <$> Just True <*> Just False" ==> Right (tyMaybe tyBool, Just True , "(\\x0 -> (\\x1 -> x0 `xor` x1)) <$> Just True <*> Just False")
- , "Just False <* Just True"          ==> Right (tyMaybe tyBool, Just False, "Just False <* Just True")
- , "Just False *> Just True"          ==> Right (tyMaybe tyBool, Just True , "Just False *> Just True")
- ]
diff --git a/Language/Symantic/Lib/Bool.hs b/Language/Symantic/Lib/Bool.hs
--- a/Language/Symantic/Lib/Bool.hs
+++ b/Language/Symantic/Lib/Bool.hs
@@ -58,8 +58,8 @@
 instance NameTyOf Bool where
 	nameTyOf _c = ["Bool"] `Mod` "Bool"
 instance ClassInstancesFor Bool where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
-	 | Just HRefl <- proj_ConstKiTy @_ @Bool c
+	proveConstraintFor _ (TyConst _ _ q :@ b)
+	 | Just HRefl <- proj_ConstKiTy @_ @Bool b
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
 		   | Just Refl <- proj_Const @Enum    q -> Just Dict
diff --git a/Language/Symantic/Lib/Bool/Test.hs b/Language/Symantic/Lib/Bool/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Bool/Test.hs
+++ /dev/null
@@ -1,86 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Bool.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
-
-import Language.Symantic
-import Language.Symantic.Lib
--- import Language.Symantic.Lib.Lambda ((~>))
-import Compiling.Test
-
-type SS =
- [ Proxy Bool
- , Proxy (->)
- , Proxy Integer
- , Proxy []
- , Proxy Char
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Bool" $
- [ "True"                           ==> Right (tyBool, True , "True")
- , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")
- , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")
- , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")
- , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")
- , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")
- , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")
- , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")
- , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")
- , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")
- , testGroup "Error_Term"
-	 [ "True True" ==> Left (tyBool,
-		Right $ Error_Term_Beta $
-		Error_Beta_Term_not_a_function $
-		TypeVT $ tyBool @_ @'[])
-	 , "x" ==> Left (tyBool,
-		Right $ Error_Term_unknown $ NameTe "x")
-	 , "x `xor` True" ==> Left (tyBool,
-		Right $ Error_Term_unknown $ NameTe "x")
-	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,
-		Right $ Error_Term_unknown $ NameTe "Bool")
-	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,
-		Right $ Error_Term_Beta $
-		Error_Beta_Term_not_a_function $
-		TypeVT $ tyBool @_ @'[])
-	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,
-		Right $ Error_Term_Beta $ Error_Beta_Unify $
-		Error_Unify_Const_mismatch
-		 (TypeVT $ tyFun @_ @'[])
-		 (TypeVT $ tyBool @_ @'[]))
-	 ]
- ]
-
--- * Class 'Sym_Bool_Vars'
--- | A few boolean variables.
-class Sym_Bool_Vars repr where
-	x :: repr Bool
-	y :: repr Bool
-	z :: repr Bool
-instance Sym_Bool_Vars View where
-	x = View $ \_p _v -> "x"
-	y = View $ \_p _v -> "y"
-	z = View $ \_p _v -> "z"
-{-
-instance -- Trans_Boo_Const
- ( Sym_Bool repr
- , Sym_Bool_Vars repr
- ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
-	x = trans_lift x
-	y = trans_lift y
-	z = trans_lift z
--}
-
--- * EDSL tests
-te1 = bool True && bool False
-te2 = (bool True && bool False) ||  (bool True && bool True)
-te3 = (bool True ||  bool False) && (bool True ||  bool True)
-te4 = bool True && not (bool False)
-te5 = bool True && not x
-te6 = x `xor` y
-te7 = (x `xor` y) `xor` z
-te8 = x `xor` (y `xor` bool True)
diff --git a/Language/Symantic/Lib/Char.hs b/Language/Symantic/Lib/Char.hs
--- a/Language/Symantic/Lib/Char.hs
+++ b/Language/Symantic/Lib/Char.hs
@@ -6,7 +6,7 @@
 import qualified Data.Char as Char
 import qualified Data.Text as Text
 
-import Language.Symantic.Grammar hiding (char, any)
+import Language.Symantic.Grammar hiding (char)
 import qualified Language.Symantic.Grammar as G
 import Language.Symantic
 import Language.Symantic.Lib.List (tyList)
@@ -48,7 +48,7 @@
 instance NameTyOf Char where
 	nameTyOf _c = ["Char"] `Mod` "Char"
 instance ClassInstancesFor Char where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :@ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Char z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
@@ -78,7 +78,7 @@
 		 )
 	 ]
 		where
-		tickG :: Gram_Terminal g' => g' Char
+		tickG :: Gram_Char g' => g' Char
 		tickG = G.char '\''
 instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
 	moduleFor = ["Char"] `moduleWhere`
diff --git a/Language/Symantic/Lib/Either.hs b/Language/Symantic/Lib/Either.hs
--- a/Language/Symantic/Lib/Either.hs
+++ b/Language/Symantic/Lib/Either.hs
@@ -48,8 +48,8 @@
 	nameTyOf _c = ["Either"] `Mod` "Either"
 instance FixityOf Either
 instance ClassInstancesFor Either where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
-	 | Just HRefl <- proj_ConstKiTy @_ @Either c
+	proveConstraintFor _ (TyConst _ _ q :$ e:@_l)
+	 | Just HRefl <- proj_ConstKiTy @_ @Either e
 	 = case () of
 		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
 		   | Just Refl <- proj_Const @Applicative q -> Just Dict
@@ -57,26 +57,26 @@
 		   | Just Refl <- proj_Const @Foldable    q -> Just Dict
 		   | Just Refl <- proj_Const @Traversable q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
-	 | Just HRefl <- proj_ConstKiTy @_ @Either c
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ e:@l:@r)
+	 | Just HRefl <- proj_ConstKiTy @_ @Either e
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` l)
-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`l)
+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
-		   , Just Dict <- proveConstraint (tq `tyApp` l)
-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`l)
+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` l)
-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`l)
+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Either where
-	expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
+	expandFamFor _c _len f (e:@_ty_l:@r `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
-	 , Just HRefl <- proj_ConstKiTy @_ @Either c
+	 , Just HRefl <- proj_ConstKiTy @_ @Either e
 	 = Just r
 	expandFamFor _c _len _fam _as = Nothing
 
diff --git a/Language/Symantic/Lib/Foldable.hs b/Language/Symantic/Lib/Foldable.hs
--- a/Language/Symantic/Lib/Foldable.hs
+++ b/Language/Symantic/Lib/Foldable.hs
@@ -10,7 +10,7 @@
 import qualified Data.Foldable as Foldable
 import Prelude hiding (Foldable(..)
  , all, and, any, concat, concatMap
- , mapM_, notElem, or, sequence, sequence_)
+ , mapM_, notElem, or, sequence_)
 
 import Language.Symantic
 import Language.Symantic.Lib.Alternative (tyAlternative)
diff --git a/Language/Symantic/Lib/Foldable/Test.hs b/Language/Symantic/Lib/Foldable/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Foldable/Test.hs
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Foldable.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
-
-import Language.Symantic.Lib
-import Compiling.Test
-
-type SS =
- [ Proxy (->)
- , Proxy Int
- , Proxy Integer
- , Proxy []
- , Proxy ()
- , Proxy (,)
- , Proxy Foldable
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Foldable"
- [ {-"[]" ==> Right (tyList (tyVar "a" varZ), [], "[]")
- ,-} "[1, 2, 3]" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")
- , "1 : 2 : 3 : []" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")
- , "foldMap (\\(x0:Integer) -> [x0, x0]) [1, 2, 3]" ==> Right
-	 ( tyList tyInteger
-	 , [1, 1, 2, 2, 3, 3]
-	 , "foldMap (\\x0 -> x0 : x0 : []) (1 : 2 : 3 : [])" )
- ]
diff --git a/Language/Symantic/Lib/Function.hs b/Language/Symantic/Lib/Function.hs
--- a/Language/Symantic/Lib/Function.hs
+++ b/Language/Symantic/Lib/Function.hs
@@ -49,19 +49,19 @@
 instance NameTyOf (->) where
 	nameTyOf _c = [] `Mod` "->"
 instance ClassInstancesFor (->) where
-	proveConstraintFor _c (TyApp _ q (TyApp _ z _r))
-	 | Just HRefl <- proj_ConstKiTy @_ @(->) z
+	proveConstraintFor _c (TyConst _ _ q :$ f:@_r)
+	 | Just HRefl <- proj_ConstKiTy @_ @(->) f
 	 = case () of
-		 _ | Just HRefl <- proj_ConstKiTy @_ @Functor     q -> Just Dict
-		   | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict
-		   | Just HRefl <- proj_ConstKiTy @_ @Monad       q -> Just Dict
+		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
+		   | Just Refl <- proj_Const @Applicative q -> Just Dict
+		   | Just Refl <- proj_Const @Monad       q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b))
-	 | Just HRefl <- proj_ConstKiTy @_ @(->) z
+	proveConstraintFor _c (tq@(TyConst _ _ q) :$ f:@_a:@b)
+	 | Just HRefl <- proj_ConstKiTy @_ @(->) f
 	 = case () of
-		 _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q
-		   , Just Dict  <- proveConstraint (q `tyApp` b) -> Just Dict
-		   | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict
+		 _ | Just Refl <- proj_Const @Monoid q
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
+		   | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (->)
@@ -74,7 +74,7 @@
 	 , "flip"  := teFunction_flip
 	 , "id"    := teFunction_id
 	 , "." `withInfixR` 9 := teFunction_compose
-	 -- , "$" `withInfixR` 0 := teFunction_app
+	 , "$" `withInfixR` 0 := teFunction_apply
 	 ]
 
 -- ** 'Type's
@@ -105,3 +105,6 @@
 
 teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))
 teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id
+
+teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))
+teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply
diff --git a/Language/Symantic/Lib/Functor/Test.hs b/Language/Symantic/Lib/Functor/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Functor/Test.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Functor.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
-
-import Language.Symantic ()
-import Language.Symantic.Lib
-import Compiling.Test
-
-type SS =
- [ Proxy (->)
- , Proxy Bool
- , Proxy Functor
- , Proxy Integer
- , Proxy Maybe
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Functor"
- [ "fmap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")
- , "not `fmap` Just True" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")
- , "not <$> Just True"    ==> Right (tyMaybe tyBool, Just False, "(\\x0 -> not x0) <$> Just True")
- , "False <$ Just True"   ==> Right (tyMaybe tyBool, Just False, "False <$ Just True")
- ]
diff --git a/Language/Symantic/Lib/IO.hs b/Language/Symantic/Lib/IO.hs
--- a/Language/Symantic/Lib/IO.hs
+++ b/Language/Symantic/Lib/IO.hs
@@ -60,28 +60,28 @@
 	nameTyOf _c = ["IO"] `Mod` "IOMode"
 instance FixityOf IO
 instance ClassInstancesFor IO where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @IO z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
 		   | Just Refl <- proj_Const @Functor     q -> Just Dict
 		   | Just Refl <- proj_Const @Monad       q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ q (TyApp _ z _a))
+	proveConstraintFor _ (TyConst _ _ q :$ z:@_a)
 	 | Just HRefl <- proj_ConstKiTy @_ @IO z
 	 = case () of
-		 _ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict
+		 _ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance ClassInstancesFor IO.Handle where
-	proveConstraintFor _ (TyApp _ q z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
 	 = case () of
-		 _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict
+		 _ | Just Refl <- proj_Const @Eq q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance ClassInstancesFor IO.IOMode where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
+	proveConstraintFor _ (TyConst _ _ q :$ c)
 	 | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c
 	 = case () of
 		 _ | Just Refl <- proj_Const @Enum q -> Just Dict
@@ -90,7 +90,7 @@
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor IO where
-	expandFamFor _c _len f (TyApp _ z a `TypesS` TypesZ)
+	expandFamFor _c _len f (z:@a `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
 	 , Just HRefl <- proj_ConstKiTy @_ @IO z
 	 = Just a
diff --git a/Language/Symantic/Lib/Int.hs b/Language/Symantic/Lib/Int.hs
--- a/Language/Symantic/Lib/Int.hs
+++ b/Language/Symantic/Lib/Int.hs
@@ -30,7 +30,7 @@
 instance NameTyOf Int where
 	nameTyOf _c = ["Int"] `Mod` "Int"
 instance ClassInstancesFor Int where
-	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _c (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Int z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
diff --git a/Language/Symantic/Lib/Integer.hs b/Language/Symantic/Lib/Integer.hs
--- a/Language/Symantic/Lib/Integer.hs
+++ b/Language/Symantic/Lib/Integer.hs
@@ -31,7 +31,7 @@
 instance NameTyOf Integer where
 	nameTyOf _c = ["Integer"] `Mod` "Integer"
 instance ClassInstancesFor Integer where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Integer z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Enum     q -> Just Dict
diff --git a/Language/Symantic/Lib/List.hs b/Language/Symantic/Lib/List.hs
--- a/Language/Symantic/Lib/List.hs
+++ b/Language/Symantic/Lib/List.hs
@@ -66,7 +66,7 @@
 	nameTyOf _c = [] `Mod` "[]"
 instance FixityOf []
 instance ClassInstancesFor [] where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @[] z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
@@ -75,16 +75,16 @@
 		   | Just Refl <- proj_Const @Monad       q -> Just Dict
 		   | Just Refl <- proj_Const @Traversable q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ z:@a)
 	 | Just HRefl <- proj_ConstKiTy @_ @[] z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Monoid q -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict
 		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict
@@ -92,7 +92,7 @@
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor [] where
-	expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)
+	expandFamFor _c _len f (z:@a `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi   @_ @Element f
 	 , Just HRefl <- proj_ConstKiTy @_ @[] z
 	 = Just a
diff --git a/Language/Symantic/Lib/Map.hs b/Language/Symantic/Lib/Map.hs
--- a/Language/Symantic/Lib/Map.hs
+++ b/Language/Symantic/Lib/Map.hs
@@ -89,34 +89,34 @@
 	nameTyOf _c = ["Map"] `Mod` "Map"
 instance FixityOf Map
 instance ClassInstancesFor Map where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
-	 | Just HRefl <- proj_ConstKiTy @_ @Map c
+	proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
+	 | Just HRefl <- proj_ConstKiTy @_ @Map m
 	 = case () of
 		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
 		   | Just Refl <- proj_Const @Foldable    q -> Just Dict
 		   | Just Refl <- proj_Const @Traversable q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))
-	 | Just HRefl <- proj_ConstKiTy @_ @Map c
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
+	 | Just HRefl <- proj_ConstKiTy @_ @Map m
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` k)
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`k)
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
-		   , Just Dict <- proveConstraint (tq `tyApp` k)
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`k)
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Monoid q
 		   , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` k)
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`k)
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Map where
-	expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)
+	expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
-	 , Just HRefl <- proj_ConstKiTy @_ @Map c
+	 , Just HRefl <- proj_ConstKiTy @_ @Map m
 	 = Just a
 	expandFamFor _c _len _fam _as = Nothing
 
diff --git a/Language/Symantic/Lib/Map/Test.hs b/Language/Symantic/Lib/Map/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Map/Test.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Map.Test where
-
-import Test.Tasty
-
-import Data.Map.Strict (Map)
-import Data.Proxy (Proxy(..))
-import Data.Text as Text
-import Prelude hiding (zipWith)
-import qualified Data.Map.Strict as Map
-
-import Language.Symantic.Lib
-import Compiling.Test
-
-type SS =
- [ Proxy (->)
- , Proxy []
- , Proxy Int
- , Proxy Integer
- , Proxy Map
- , Proxy Char
- , Proxy (,)
- , Proxy Num
- , Proxy Monoid
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Map"
- [ "Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c'])" ==> Right
-	 ( tyMap tyInteger tyChar
-	 , Map.fromList [(1, 'a'), (2, 'b'), (3, 'c')]
-	 , "Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : []))" )
- , Text.concat
-	[ "Map.foldrWithKey"
-	, " (\\(k:Integer) (v:Char) (acc:(Integer,[Char])) ->"
-	, "  (k + fst acc, v : snd acc))"
-	, " (0, [])"
-	, " (Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c']))"
-	] ==> Right
-	 ( tyInteger `tyTuple2` tyString
-	 , (6, "abc")
-	 , "Map.foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, x1 : snd x2)))) (0, []) (Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : [])))" )
- ]
diff --git a/Language/Symantic/Lib/Maybe.hs b/Language/Symantic/Lib/Maybe.hs
--- a/Language/Symantic/Lib/Maybe.hs
+++ b/Language/Symantic/Lib/Maybe.hs
@@ -49,32 +49,32 @@
 	nameTyOf _c = ["Maybe"] `Mod` "Maybe"
 instance FixityOf Maybe
 instance ClassInstancesFor Maybe where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
-	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+	proveConstraintFor _ (TyConst _ _ q :$ m)
+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe m
 	 = case () of
 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
-		   | Just Refl <- proj_Const @Foldable q    -> Just Dict
-		   | Just Refl <- proj_Const @Functor q     -> Just Dict
-		   | Just Refl <- proj_Const @Monad q       -> Just Dict
+		   | Just Refl <- proj_Const @Foldable    q -> Just Dict
+		   | Just Refl <- proj_Const @Functor     q -> Just Dict
+		   | Just Refl <- proj_Const @Monad       q -> Just Dict
 		   | Just Refl <- proj_Const @Traversable q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
-	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@a)
+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe m
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Monoid q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Maybe where
-	expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
+	expandFamFor _c _len f (m:@a `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
-	 , Just HRefl <- proj_ConstKiTy @_ @Maybe c
+	 , Just HRefl <- proj_ConstKiTy @_ @Maybe m
 	 = Just a
 	expandFamFor _c _len _fam _as = Nothing
 
diff --git a/Language/Symantic/Lib/MonoFunctor.hs b/Language/Symantic/Lib/MonoFunctor.hs
--- a/Language/Symantic/Lib/MonoFunctor.hs
+++ b/Language/Symantic/Lib/MonoFunctor.hs
@@ -16,7 +16,7 @@
 	nameTyOf _c = ["MonoFunctor"] `Mod` "Element"
 instance ClassInstancesFor Element
 instance TypeInstancesFor Element where
-	expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)
+	expandFamFor _c _len f (z:@_ty_r:@ a `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
 	 , Just HRefl <- proj_ConstKiTy @_ @(->) z
 	 = Just a
@@ -30,11 +30,11 @@
 type instance Sym MonoFunctor = Sym_MonoFunctor
 class Sym_MonoFunctor term where
 	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
-	default omap
-	 :: Sym_MonoFunctor (UnT term)
-	 => Trans term
-	 => MonoFunctor o
-	 => term (MT.Element o -> MT.Element o) -> term o -> term o
+	default omap ::
+	 Sym_MonoFunctor (UnT term) =>
+	 Trans term =>
+	 MonoFunctor o =>
+	 term (MT.Element o -> MT.Element o) -> term o -> term o
 	omap = trans2 omap
 
 -- Interpreting
diff --git a/Language/Symantic/Lib/MonoFunctor/Test.hs b/Language/Symantic/Lib/MonoFunctor/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/MonoFunctor/Test.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.MonoFunctor.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding (zipWith)
-import qualified Data.MonoTraversable as MT
-
-import Language.Symantic.Lib
-import Compiling.Test
-
-type SS =
- [ Proxy (->)
- , Proxy []
- , Proxy Integer
- , Proxy Bool
- , Proxy Char
- , Proxy MT.MonoFunctor
- , Proxy Maybe
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "MonoFunctor"
- [ "omap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "omap (\\x0 -> not x0) (Just True)")
- , "omap Char.toUpper ['a', 'b', 'c']" ==> Right (tyList tyChar, "ABC", "omap (\\x0 -> Char.toUpper x0) ('a' : 'b' : 'c' : [])" )
- ]
diff --git a/Language/Symantic/Lib/NonNull.hs b/Language/Symantic/Lib/NonNull.hs
--- a/Language/Symantic/Lib/NonNull.hs
+++ b/Language/Symantic/Lib/NonNull.hs
@@ -89,27 +89,27 @@
 	nameTyOf _c = ["NonNull"] `Mod` "NonNull"
 instance FixityOf NonNull
 instance TypeInstancesFor NonNull where
-	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
+	expandFamFor c len f (z:@o `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
 	 , Just HRefl <- proj_ConstKiTy @_ @NonNull z
 	 = expandFamFor c len f (o `TypesS` TypesZ)
 	expandFamFor _c _len _fam _as = Nothing
 instance ClassInstancesFor NonNull where
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@o)
 	 | Just HRefl <- proj_ConstKiTy @_ @NonNull c
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFoldable q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFunctor q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		   | Just Refl <- proj_Const @SemiSequence q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 
diff --git a/Language/Symantic/Lib/Num/Test.hs b/Language/Symantic/Lib/Num/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Num/Test.hs
+++ /dev/null
@@ -1,98 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Lib.Num.Test where
-
-import Test.Tasty
-
-import Prelude (Num)
-import Prelude hiding (Num(..))
-
-import Language.Symantic
-import Language.Symantic.Lib
-import Compiling.Test
-
--- * Tests
-type SS =
- [ Proxy (->)
- , Proxy Integer
- , Proxy Num
- , Proxy Num2
- , Proxy Int
- , Proxy Integral
- , Proxy Foldable
- , Proxy Traversable
- , Proxy []
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Num"
- [ "42"                        ==> Right (tyInteger,  42, "42")
- , "-42"                       ==> Right (tyInteger, -42, "negate 42")
- , "- -42"                     ==> Right (tyInteger,  42, "negate (negate 42)")
- , "1 + -2"                    ==> Right (tyInteger,  -1, "1 + negate 2")
- , "-1 + -2"                   ==> Right (tyInteger,  -3, "negate 1 + negate 2")
- , "-(1 + -2)"                 ==> Right (tyInteger,   1, "negate (1 + negate 2)")
- , "(+) 1 2"                   ==> Right (tyInteger,   3, "1 + 2")
- , "1 + 2"                     ==> Right (tyInteger,   3, "1 + 2")
- , "1 + 2 - 3"                 ==> Right (tyInteger,   0, "1 + 2 - 3")
- , "1 + 2 * 3"                 ==> Right (tyInteger,   7, "1 + 2 * 3")
- , "3 * 2 + 1"                 ==> Right (tyInteger,   7, "3 * 2 + 1")
- , "3 * (2 + 1)"               ==> Right (tyInteger,   9, "3 * (2 + 1)")
- , "4 + 3 * 2 + 1"             ==> Right (tyInteger,  11, "4 + 3 * 2 + 1")
- , "5 * 4 + 3 * 2 + 1"         ==> Right (tyInteger,  27, "5 * 4 + 3 * 2 + 1")
- , "negate`42"                 ==> Right (tyInteger, -42, "negate 42")
- , "42`negate"                 ==> Right (tyInteger, -42, "negate 42")
- , "42`negate "                ==> Right (tyInteger, -42, "negate 42")
- , "42`negate`negate"          ==> Right (tyInteger,  42, "negate (negate 42)")
- , "42`abs`negate"             ==> Right (tyInteger, -42, "negate (abs 42)")
- , "42`negate`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")
- , "abs`negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")
- , "negate`abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")
- , "negate`abs`42`mod`9"       ==> Right (tyInteger,   3, "negate (abs 42) `mod` 9")
- , "negate abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")
- , "negate 42`abs"             ==> Right (tyInteger, -42, "negate (abs 42)")
- , "(+) negate`2 44"           ==> Right (tyInteger,  42, "negate 2 + 44")
- , "(+) 2`negate 44"           ==> Right (tyInteger,  42, "negate 2 + 44")
- , "(+) (negate`2) 44"         ==> Right (tyInteger,  42, "negate 2 + 44")
- , "abs negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")
- , "(+) 40 2"                  ==> Right (tyInteger,  42, "40 + 2")
- , "(+) 40 -2"                 ==> Right (tyInteger,  38, "40 + negate 2")
- , "negate 42 + 42`negate"     ==> Right (tyInteger, -84, "negate 42 + negate 42")
- , "(+) (negate 42) 42`negate" ==> Right (tyInteger, -84, "negate 42 + negate 42")
- , "(+) negate`42 42`negate"   ==> Right (tyInteger, -84, "negate 42 + negate 42")
- , "42`abs`negate`mod`abs`negate`9" ==> Right (tyInteger, 3, "negate (abs 42) `mod` abs (negate 9)")
- , "abs`42`negate"             ==> Right (tyInteger,  42, "abs (negate 42)")
- , "negate`42`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")
- , testGroup "Error_Term"
-	 [ "(+) 40 - 2" ==> Left (tyInteger,
-		Right $ Error_Term_Beta $ Error_Beta_Unify $
-		Error_Unify_Const_mismatch
-		 (TypeVT $ tyFun @_ @'[])
-		 (TypeVT $ tyInteger @_ @'[]))
-	 ]
- ]
-
--- | A newtype to test prefix and postfix.
-newtype Num2 a = Num2 a
-type instance Sym Num2 = Sym_Num2
-class Sym_Num2 (term:: * -> *) where
-
-instance Sym_Num2 Eval where
-instance Sym_Num2 View where
-instance Sym_Num2 (Dup r1 r2) where
-instance Sym_Num2 term => Sym_Num2 (BetaT term) where
-instance NameTyOf Num2 where
-	nameTyOf _c = ["Num2"] `Mod` "Num2"
-instance FixityOf Num2
-instance ClassInstancesFor Num2
-instance TypeInstancesFor Num2
-instance Gram_Term_AtomsFor src ss g Num2
-instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where
-	moduleFor = ["Num2"] `moduleWhere`
-	 [ "abs"    `withPrefix`   9 := teNum_abs
-	 , "negate" `withPrefix`  10 := teNum_negate
-	 , "abs"    `withPostfix`  9 := teNum_abs
-	 , "negate" `withPostfix` 10 := teNum_negate
-	 ]
diff --git a/Language/Symantic/Lib/Ord.hs b/Language/Symantic/Lib/Ord.hs
--- a/Language/Symantic/Lib/Ord.hs
+++ b/Language/Symantic/Lib/Ord.hs
@@ -116,7 +116,7 @@
 	nameTyOf _c = ["Ord"] `Mod` "Ord"
 instance FixityOf Ord
 instance ClassInstancesFor Ord where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @Ordering z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
diff --git a/Language/Symantic/Lib/Ratio.hs b/Language/Symantic/Lib/Ratio.hs
--- a/Language/Symantic/Lib/Ratio.hs
+++ b/Language/Symantic/Lib/Ratio.hs
@@ -47,13 +47,13 @@
 	nameTyOf _c = ["Ratio"] `Mod` "Ratio"
 instance FixityOf Ratio
 instance ClassInstancesFor Ratio where
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a)
 	 | Just HRefl <- proj_ConstKiTy @_ @Ratio c
 	 = case () of
 		 _ | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
 		   | Just Refl <- proj_Const @Real q
 		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
diff --git a/Language/Symantic/Lib/Test.hs b/Language/Symantic/Lib/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Test.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Test where
-
-import Test.Tasty
-
-import Prelude hiding ((&&), not, (||), (==), id)
-
-import Language.Symantic
-import Language.Symantic.Lib
-
-import qualified Lib.Applicative.Test as Applicative
-import qualified Lib.Bool.Test as Bool
-import qualified Lib.Foldable.Test as Foldable
-import qualified Lib.Functor.Test as Functor
-import qualified Lib.Map.Test as Map
-import qualified Lib.MonoFunctor.Test as MonoFunctor
-import qualified Lib.Num.Test as Num
-import qualified Lib.Tuple2.Test as Tuple2
-
--- * Tests
-tests :: TestTree
-tests = testGroup "Lib" $
- [ Applicative.tests
- , Bool.tests
- , Foldable.tests
- , Functor.tests
- , Map.tests
- , MonoFunctor.tests
- , Num.tests
- , Tuple2.tests
- ]
-
--- * EDSL tests
-te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)
-te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)
-te3 = let_ (bool True) $ \x -> x && x
-te4 = let_ (lam $ \x -> x && x) $ \f -> f `app` bool True
-te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1
-te6 = let_ (bool True) id && bool False
-te7 = lam $ \f -> (f  `app` bool True) && bool True
-te8 = lam $ \f -> f `app` (bool True && bool True)
diff --git a/Language/Symantic/Lib/Text.hs b/Language/Symantic/Lib/Text.hs
--- a/Language/Symantic/Lib/Text.hs
+++ b/Language/Symantic/Lib/Text.hs
@@ -8,7 +8,7 @@
 import qualified Data.Sequences as Seqs
 import qualified Data.Text as Text
 
-import Language.Symantic.Grammar
+import Language.Symantic.Grammar hiding (text)
 import Language.Symantic
 import Language.Symantic.Lib.Char ()
 import Language.Symantic.Lib.MonoFunctor (Element)
@@ -36,17 +36,17 @@
 instance NameTyOf Text where
 	nameTyOf _c = ["Text"] `Mod` "Text"
 instance ClassInstancesFor Text where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
+	proveConstraintFor _ (TyConst _ _ q :$ c)
 	 | Just HRefl <- proj_ConstKiTy @_ @Text c
 	 = case () of
-		 _ | Just Refl <- proj_Const @Eq q                -> Just Dict
-		   | Just Refl <- proj_Const @MT.MonoFoldable q   -> Just Dict
-		   | Just Refl <- proj_Const @MT.MonoFunctor q    -> Just Dict
-		   | Just Refl <- proj_Const @Monoid q            -> Just Dict
-		   | Just Refl <- proj_Const @Ord q               -> Just Dict
-		   | Just Refl <- proj_Const @Seqs.IsSequence q   -> Just Dict
+		 _ | Just Refl <- proj_Const @Eq                q -> Just Dict
+		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict
+		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict
+		   | Just Refl <- proj_Const @Monoid            q -> Just Dict
+		   | Just Refl <- proj_Const @Ord               q -> Just Dict
+		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict
 		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
-		   | Just Refl <- proj_Const @Show q              -> Just Dict
+		   | Just Refl <- proj_Const @Show              q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor Text where
diff --git a/Language/Symantic/Lib/Tuple2.hs b/Language/Symantic/Lib/Tuple2.hs
--- a/Language/Symantic/Lib/Tuple2.hs
+++ b/Language/Symantic/Lib/Tuple2.hs
@@ -55,8 +55,8 @@
 instance FixityOf (,) where
 	fixityOf _c = Just $ Fixity2 $ infixN (-1)
 instance ClassInstancesFor (,) where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))
-	 | Just HRefl <- proj_ConstKiTy @_ @(,) c
+	proveConstraintFor _ (TyConst _ _ q :$ t:@a)
+	 | Just HRefl <- proj_ConstKiTy @_ @(,) t
 	 = case () of
 		 _ | Just Refl <- proj_Const @Applicative q
 		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
@@ -66,32 +66,32 @@
 		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
 		   | Just Refl <- proj_Const @Traversable q -> Just Dict
 		 _ -> Nothing
-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))
-	 | Just HRefl <- proj_ConstKiTy @_ @(,) c
+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ t:@a:@b)
+	 | Just HRefl <- proj_ConstKiTy @_ @(,) t
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded q
-		   , Just Dict <- proveConstraint (tq `tyApp` a)
-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
 		   | Just Refl <- proj_Const @Eq q
-		   , Just Dict <- proveConstraint (tq `tyApp` a)
-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
 		   | Just Refl <- proj_Const @Monoid q
-		   , Just Dict <- proveConstraint (tq `tyApp` a)
-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
 		   | Just Refl <- proj_Const @Ord q
-		   , Just Dict <- proveConstraint (tq `tyApp` a)
-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
 		   | Just Refl <- proj_Const @Show q
-		   , Just Dict <- proveConstraint (tq `tyApp` a)
-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict
+		   , Just Dict <- proveConstraint (tq`tyApp`a)
+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
-		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict
+		   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
 		 _ -> Nothing
 	proveConstraintFor _c _q = Nothing
 instance TypeInstancesFor (,) where
-	expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)
+	expandFamFor _c _len f (t:@_a:@b `TypesS` TypesZ)
 	 | Just HRefl <- proj_ConstKi @_ @Element f
-	 , Just HRefl <- proj_ConstKiTy @_ @(,) c
+	 , Just HRefl <- proj_ConstKiTy @_ @(,) t
 	 = Just b
 	expandFamFor _c _len _fam _as = Nothing
 
diff --git a/Language/Symantic/Lib/Tuple2/Test.hs b/Language/Symantic/Lib/Tuple2/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Lib/Tuple2/Test.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-module Lib.Tuple2.Test where
-
-import Test.Tasty
-
-import Data.Proxy (Proxy(..))
-import Prelude hiding ((&&), not, (||))
-
-import Language.Symantic.Lib
-import Compiling.Test
-
-type SS =
- [ Proxy (->)
- , Proxy Integer
- , Proxy ()
- , Proxy (,)
- ]
-(==>) = readTe @() @SS
-
-tests :: TestTree
-tests = testGroup "Tuple2"
- [ "()"             ==> Right (tyUnit, (), "()")
- , "(,) 1 2"        ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")
- , "(1,2)"          ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")
- , "((1,2), (3,4))" ==> Right
-	 ( let t = tyTuple2 tyInteger tyInteger in tyTuple2 t t
-	 , ((1,2),(3,4))
-	 , "((1, 2), (3, 4))" )
- ]
diff --git a/Language/Symantic/Lib/Unit.hs b/Language/Symantic/Lib/Unit.hs
--- a/Language/Symantic/Lib/Unit.hs
+++ b/Language/Symantic/Lib/Unit.hs
@@ -3,8 +3,6 @@
 -- | Symantic for '()'.
 module Language.Symantic.Lib.Unit where
 
-import Prelude hiding ((&&), not, (||))
-
 import Language.Symantic
 import Language.Symantic.Grammar
 
@@ -30,7 +28,7 @@
 instance NameTyOf () where
 	nameTyOf _c = [] `Mod` ""
 instance ClassInstancesFor () where
-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+	proveConstraintFor _ (TyConst _ _ q :$ z)
 	 | Just HRefl <- proj_ConstKiTy @_ @() z
 	 = case () of
 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
diff --git a/Language/Symantic/Test.hs b/Language/Symantic/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Test.hs
+++ /dev/null
@@ -1,14 +0,0 @@
-module Test where
-
-import Test.Tasty
-
-import qualified Typing.Test as Typing
-import qualified Lib.Test as Lib
-
-main :: IO ()
-main =
-	defaultMain $
-	testGroup "Language.Symantic"
-	 [ Typing.tests
-	 , Lib.tests
-	 ]
diff --git a/Language/Symantic/Typing/Test.hs b/Language/Symantic/Typing/Test.hs
deleted file mode 100644
--- a/Language/Symantic/Typing/Test.hs
+++ /dev/null
@@ -1,185 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Typing.Test where
-
-import Test.Tasty
-import Test.Tasty.HUnit
-
-import Control.Applicative (Applicative(..))
-import Control.Arrow (left)
-import Data.Functor.Identity (Identity(..))
-import Data.List.NonEmpty (NonEmpty)
-import Data.Map.Strict (Map)
-import Data.Maybe (isJust)
-import Data.NonNull (NonNull)
-import Data.Proxy
-import Data.Ratio (Ratio)
-import Data.Text (Text)
-import GHC.Exts (Constraint)
-import Prelude hiding (exp)
-import qualified Control.Monad.Classes.Run as MC
-import qualified Control.Monad.Trans.State.Strict as SS
-import qualified Data.Function as Fun
-import qualified Data.Map.Strict as Map
-import qualified Data.MonoTraversable as MT
-import qualified Data.Sequences as Seqs
-import qualified System.IO as IO
-import qualified Text.Megaparsec as P
-import qualified Text.Megaparsec.Prim as P
-
-import Language.Symantic.Grammar
-import Language.Symantic
-import Language.Symantic.Lib hiding ((<$>), (<*), show)
-
-import Grammar.Megaparsec ()
-
--- * Tests
-type SS =
- [ Proxy (->)
- , Proxy Bool
- , Proxy []
- , Proxy ()
- , Proxy (,)
- , Proxy Char
- , Proxy Either
- , Proxy Int
- , Proxy Integer
- , Proxy IO
- , Proxy IO.Handle
- , Proxy IO.IOMode
- , Proxy Ordering
- , Proxy Map
- , Proxy Maybe
- , Proxy NonNull
- , Proxy Ratio
- , Proxy Text
- , Proxy Applicative
- , Proxy Bounded
- , Proxy Enum
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Integral
- , Proxy Monad
- , Proxy Monoid
- , Proxy MT.MonoFoldable
- , Proxy MT.MonoFunctor
- , Proxy Num
- , Proxy Ord
- , Proxy Real
- , Proxy Seqs.IsSequence
- , Proxy Seqs.SemiSequence
- , Proxy Show
- , Proxy Traversable
- ]
-type SRC = SrcTe (NonEmpty P.SourcePos) SS
-
-impsTy :: Imports NameTy
-impsTy = importTypes @SS []
-
-modsTy :: Source src => ModulesTy src
-modsTy =
-	Map.insert ([] `Mod` "String")
-	 (TypeTLen $ \len -> TypeT $
-		tyConstLen @(K [])   @[]   len `tyApp`
-		tyConstLen @(K Char) @Char len) $
-	modulesTyInj @SS
-
-parseTy ::
- forall src g err inp.
- g ~ P.ParsecT err inp (SS.StateT (Imports NameTy, ModulesTy src) Identity) =>
- P.MonadParsec err inp (P.ParsecT err inp g) =>
- Gram_Type src g =>
- P.Token inp ~ Char =>
- inp -> Either (P.ParseError Char err) (AST_Type src)
-parseTy inp =
-	runIdentity $
-	MC.evalStateStrict (impsTy, modsTy @src) $
-	P.runParserT g "" inp
-	where g = unCF $ g_type <* eoi
-
-tests :: TestTree
-tests = testGroup "Typing" $
- [ testGroup "readType" $
-	let run inp (TypeT exp :: TypeT SRC '[]) =
-		testCase inp $ got @?= Right (Right $ TypeVT exp)
-		where
-		got :: Either (P.ParseError Char P.Dec)
-		              (Either (Error_Type SRC) (TypeVT SRC))
-		got = readType <$> parseTy inp
-		in
-	let (==>) = run; infixr 0 ==> in
-	 [ "Bool"                        ==> TypeT $ tyBool
-	 , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool
-	 , "[]"                          ==> TypeT $ tyConst @(K []) @[]
-	 , "[Char]"                      ==> TypeT $ tyList tyChar
-	 , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)
-	 , "([])"                        ==> TypeT $ tyConst @(K []) @[]
-	 , "[()]"                        ==> TypeT $ tyList tyUnit
-	 , "()"                          ==> TypeT $ tyUnit
-	 , "(())"                        ==> TypeT $ tyUnit
-	 , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)
-	 , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)
-	 , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
-	 , "(Bool)"                      ==> TypeT $ tyBool
-	 , "((Bool))"                    ==> TypeT $ tyBool
-	 , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt
-	 , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt
-	 , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
-	 , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
-	 , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt
-	 , "String"                      ==> TypeT $ tyList tyChar
-	 , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar
-	 , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar
-	 , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool
-	 , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt
-	 , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt
-	 , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
-	 , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
-	 , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar
-	 , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
-	 , "IO"                          ==> TypeT $ tyConst @(K IO) @IO
-	 , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
-	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
-	 , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
-	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
-	 , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq
-	 , "Eq Bool"                     ==> TypeT $ tyEq tyBool
-	 ]
-	 , testGroup "Parsing errors" $
-		let run inp = testCase inp $ got @?= Left ()
-			where
-			got :: Either () (AST_Type SRC)
-			got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ parseTy inp in
-		run <$>
-		 [ "Bool, Int"
-		 , "(Bool -> Int) Char"
-		 , "NonExistingType"
-		 ]
-	 , testGroup "Compiling errors" $
-		let run inp = testCase inp $ got @?= Right (Left ())
-			where
-			got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
-			got = left (Fun.const ()) . readType <$> parseTy inp in
-		run <$>
-		 [ "Bool Int"
-		 , "[IO]"
-		 , "(->) IO"
-		 , "(->) Bool Int Char"
-		 , "Monad Eq"
-		 ]
- , testGroup "proveConstraint" $
-	let (==>) (typ::Type SRC SS (t::Constraint)) expected =
-		let imps = importTypes @SS [] in
-		let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
-		testCase (showType conf typ) $
-		isJust (proveConstraint typ) @?= expected in
-	 [ tyEq          tyBool                      ==> True
-	 , tyOrd         tyBool                      ==> True
-	 , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True
-	 , tyFunctor     (tyConst @(K IO) @IO)       ==> True
-	 , tyMonad       (tyConst @(K IO) @IO)       ==> True
-	 , tyTraversable (tyConst @(K IO) @IO)       ==> False
-	 ]
- ]
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,13 @@
+resolver: lts-10.5
+packages:
+- '.'
+- location: '../symantic'
+  extra-dep: true
+- location: '../symantic-grammar'
+  extra-dep: true
+- location: '../symantic-document'
+  extra-dep: true
+- location: '../monad-classes'
+  extra-dep: true
+extra-deps:
+- peano-0.1.0.1
diff --git a/symantic-lib.cabal b/symantic-lib.cabal
--- a/symantic-lib.cabal
+++ b/symantic-lib.cabal
@@ -1,51 +1,33 @@
-author: Julien Moutinho <julm+symantic@autogeree.net>
+name: symantic-lib
+-- PVP:  +-+------- breaking API changes
+--       | | +----- non-breaking API additions
+--       | | | +--- code changes with no API change
+version: 0.0.3.20180213
+category: Language
+synopsis: Symantics for common types.
+description: Symantics for common types,
+             using <https://hackage.haskell.org/package/symantic symantic>.
+extra-doc-files:
+license: GPL-3
+license-file: COPYING
+stability: experimental
+author:      Julien Moutinho <julm+symantic@autogeree.net>
+maintainer:  Julien Moutinho <julm+symantic@autogeree.net>
 bug-reports: Julien Moutinho <julm+symantic@autogeree.net>
+-- homepage:
+
 build-type: Simple
 cabal-version: >= 1.24
-category: Language
-description:
-  Symantics for common types,
-  using <https://hackage.haskell.org/package/symantic symantic>.
 extra-source-files:
+  stack.yaml
 extra-tmp-files:
--- homepage: 
-license: GPL-3
-license-file: COPYING
-maintainer: Julien Moutinho <julm+symantic@autogeree.net>
-name: symantic-lib
-stability: experimental
-synopsis: Symantics for common types.
-tested-with: GHC==8.0.2
--- PVP:  +-+------- breaking API changes
---       | | +----- non-breaking API additions
---       | | | +--- code changes with no API change
-version: 0.0.2.20170703
+tested-with: GHC==8.2.2
 
 Source-Repository head
   location: git://git.autogeree.net/symantic
   type:     git
 
 Library
-  default-extensions:
-    DataKinds
-    DefaultSignatures
-    FlexibleContexts
-    FlexibleInstances
-    LambdaCase
-    MultiParamTypeClasses
-    NamedFieldPuns
-    OverloadedStrings
-    Rank2Types
-    ScopedTypeVariables
-    StandaloneDeriving
-    TupleSections
-    TypeApplications
-    TypeFamilies
-    TypeOperators
-  ghc-options: -Wall
-               -fno-warn-tabs
-               -fprint-explicit-kinds
-  default-language: Haskell2010
   exposed-modules:
     Language.Symantic.Lib
     Language.Symantic.Lib.Alternative
@@ -83,102 +65,91 @@
     Language.Symantic.Lib.Traversable
     Language.Symantic.Lib.Tuple2
     Language.Symantic.Lib.Unit
-  build-depends:
-    base >= 4.6 && < 5
-    , containers
-    , ghc-prim
-    , monad-classes
-    , mono-traversable
-    , symantic >= 6.0
-    , symantic-grammar
-    , transformers
-    , text
-
-Test-Suite symantic-test
-  type: exitcode-stdio-1.0
+  default-language: Haskell2010
   default-extensions:
     DataKinds
+    DefaultSignatures
     FlexibleContexts
     FlexibleInstances
+    LambdaCase
     MultiParamTypeClasses
-    NoMonomorphismRestriction
+    NamedFieldPuns
     OverloadedStrings
+    Rank2Types
     ScopedTypeVariables
+    StandaloneDeriving
     TupleSections
     TypeApplications
     TypeFamilies
     TypeOperators
-  default-language: Haskell2010
-  ghc-options: -main-is Test
-               -Wall
-               -fno-warn-tabs
-               -- -O0
-               -- -fmax-simplifier-iterations=0
-               -- -dshow-passes
-  hs-source-dirs: Language/Symantic
-  main-is: Test.hs
-  other-modules:
-    Compiling.Test
-    Grammar.Megaparsec
-    Lib.Applicative.Test
-    Lib.Bool.Test
-    Lib.Foldable.Test
-    Lib.Functor.Test
-    Lib.Map.Test
-    Lib.MonoFunctor.Test
-    Lib.Num.Test
-    Lib.Test
-    Lib.Tuple2.Test
-    Typing.Test
+  ghc-options:
+    -Wall
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -fno-warn-tabs
+    -fhide-source-paths
+    -fprint-explicit-kinds
   build-depends:
-    base >= 4.6 && < 5
-    , containers
-    , megaparsec
-    , monad-classes
-    , mono-traversable
+      symantic
     , symantic-grammar
-    , symantic
-    , symantic-lib
-    , tasty >= 0.11
-    , tasty-hunit
-    , text
-    , transformers
+    , base             >= 4.6 && < 5
+    , containers       >= 0.5
+    , mono-traversable >= 1.0
+    , transformers     >= 0.5
+    , text             >= 1.2
 
-Test-Suite ebnf
+Test-Suite symantic-test
   type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  other-modules:
+    Golden
+    HUnit
+    HUnit.Applicative
+    HUnit.Bool
+    HUnit.Foldable
+    HUnit.Functor
+    HUnit.Map
+    HUnit.MonoFunctor
+    HUnit.Num
+    HUnit.Tuple2
+    Testing.Compiling
+    Testing.Megaparsec
+  default-language: Haskell2010
   default-extensions:
-    ConstraintKinds
     DataKinds
-    EmptyDataDecls
     FlexibleContexts
     FlexibleInstances
     MultiParamTypeClasses
-    NamedFieldPuns
+    NoMonomorphismRestriction
     OverloadedStrings
-    PatternGuards
-    PolyKinds
-    Rank2Types
     ScopedTypeVariables
-    StandaloneDeriving
     TupleSections
-    TypeFamilies
     TypeApplications
+    TypeFamilies
     TypeOperators
-  ghc-options: -main-is Grammar.EBNF
-               -Wall
-               -fno-warn-tabs
-               -fprint-potential-instances
-  main-is: Grammar/EBNF.hs
-  default-language: Haskell2010
-  hs-source-dirs: Language/Symantic
+  ghc-options:
+    -Wall
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -fno-warn-tabs
+    -fhide-source-paths
+    -fprint-explicit-kinds
+    -- -O0
+    -- -fmax-simplifier-iterations=0
+    -- -dshow-passes
   build-depends:
-    base >= 4.6 && < 5
-    , containers
-    , megaparsec
+      symantic
     , symantic-grammar
-    , symantic
     , symantic-lib
-    , transformers
-    , tasty >= 0.11
-    , tasty-hunit
-    , text
+    , base             >= 4.6 && < 5
+    , bytestring       >= 0.10
+    , containers       >= 0.5
+    , megaparsec       >= 6.3
+    , monad-classes    >= 0.3.2
+    , mono-traversable >= 1.0
+    , tasty            >= 0.11
+    , tasty-golden     >= 2.3
+    , tasty-hunit      >= 0.9
+    , text             >= 1.2
+    , transformers     >= 0.5
diff --git a/test/Golden.hs b/test/Golden.hs
new file mode 100644
--- /dev/null
+++ b/test/Golden.hs
@@ -0,0 +1,46 @@
+module Golden where
+
+import Control.Monad (Monad(..))
+import Data.Function (($), (.))
+import Data.Functor ((<$>))
+import Data.Semigroup (Semigroup(..))
+import Data.String (String)
+-- import System.FilePath (FilePath)
+import System.IO (IO)
+import qualified Data.ByteString.Lazy as BSL
+import qualified Data.List as List
+import qualified Data.Text.Lazy          as TL
+import qualified Data.Text.Lazy.Encoding as TL
+
+import Test.Tasty
+import Test.Tasty.Golden
+
+import Language.Symantic.Grammar
+import Language.Symantic
+import Language.Symantic.Lib ()
+
+-- * Golden testing utilities
+testGolden :: TestName -> TestName -> IO BSL.ByteString -> TestTree
+testGolden inputFile expectedExt =
+	goldenVsStringDiff inputFile diffGolden (inputFile <> expectedExt)
+
+diffGolden :: FilePath -> FilePath -> [String]
+diffGolden ref new = ["diff", "-u", ref, new]
+
+-- * All golden tests
+goldensIO :: IO TestTree
+goldensIO = do
+	-- inputFiles <- List.sort <$> findByExtension [".sym"] "test/Golden"
+	return $
+		testGroup "Golden"
+		 [ testGolden "grammar.ebnf" "" $ do
+			return $
+				TL.encodeUtf8 $
+				TL.unlines $
+				List.concat
+				 [ render <$> gram_comment
+				 , render <$> gram_type
+				 , render <$> gram_term
+				 ]
+		 ]
+	where render = TL.fromStrict . renderEBNF . unCF
diff --git a/test/HUnit.hs b/test/HUnit.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit where
+
+import Test.Tasty
+import Prelude hiding ((&&), not, (||), id)
+
+import Language.Symantic
+import Language.Symantic.Lib
+
+import qualified HUnit.Applicative as Applicative
+import qualified HUnit.Bool        as Bool
+import qualified HUnit.Foldable    as Foldable
+import qualified HUnit.Functor     as Functor
+import qualified HUnit.Map         as Map
+import qualified HUnit.MonoFunctor as MonoFunctor
+import qualified HUnit.Num         as Num
+import qualified HUnit.Tuple2      as Tuple2
+
+-- * Tests
+hunits :: TestTree
+hunits = testGroup "HUnit" $
+ [ Applicative.hunits
+ , Bool.hunits
+ , Foldable.hunits
+ , Functor.hunits
+ , Map.hunits
+ , MonoFunctor.hunits
+ , Num.hunits
+ , Tuple2.hunits
+ ]
+
+-- * EDSL tests
+te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)
+te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)
+te3 = let_ (bool True) $ \x -> x && x
+te4 = let_ (lam $ \x -> x && x) $ \f -> f `app` bool True
+te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1
+te6 = let_ (bool True) id && bool False
+te7 = lam $ \f -> (f  `app` bool True) && bool True
+te8 = lam $ \f -> f `app` (bool True && bool True)
diff --git a/test/HUnit/Applicative.hs b/test/HUnit/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Applicative.hs
@@ -0,0 +1,28 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Applicative where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+
+import Language.Symantic.Lib
+import Testing.Compiling
+import HUnit.Bool ()
+
+type SS =
+ [ Proxy (->)
+ , Proxy Integer
+ , Proxy Bool
+ , Proxy Maybe
+ , Proxy Functor
+ , Proxy Applicative
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Applicative"
+ [ "Just (xor True) <*> Just True"    ==> Right (tyMaybe tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True")
+ , "Just (xor True) <*> Nothing"      ==> Right (tyMaybe tyBool, Nothing   , "Just (\\x0 -> True `xor` x0) <*> Nothing")
+ , "xor <$> Just True <*> Just False" ==> Right (tyMaybe tyBool, Just True , "(\\x0 -> (\\x1 -> x0 `xor` x1)) <$> Just True <*> Just False")
+ , "Just False <* Just True"          ==> Right (tyMaybe tyBool, Just False, "Just False <* Just True")
+ , "Just False *> Just True"          ==> Right (tyMaybe tyBool, Just True , "Just False *> Just True")
+ ]
diff --git a/test/HUnit/Bool.hs b/test/HUnit/Bool.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Bool.hs
@@ -0,0 +1,84 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Bool where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+import Prelude hiding ((&&), not, (||))
+
+import Language.Symantic
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy Bool
+ , Proxy (->)
+ , Proxy Integer
+ , Proxy []
+ , Proxy Char
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Bool" $
+ [ "True"                           ==> Right (tyBool, True , "True")
+ , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")
+ , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")
+ , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")
+ , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")
+ , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")
+ , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")
+ , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")
+ , testGroup "Error_Term"
+	 [ "True True" ==> Left (tyBool,
+		Right $ Error_Term_Beta $
+		Error_Beta_Term_not_a_function $
+		TypeVT $ tyBool @_ @'[])
+	 , "x" ==> Left (tyBool,
+		Right $ Error_Term_unknown $ NameTe "x")
+	 , "x `xor` True" ==> Left (tyBool,
+		Right $ Error_Term_unknown $ NameTe "x")
+	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,
+		Right $ Error_Term_unknown $ NameTe "Bool")
+	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,
+		Right $ Error_Term_Beta $
+		Error_Beta_Term_not_a_function $
+		TypeVT $ tyBool @_ @'[])
+	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,
+		Right $ Error_Term_Beta $ Error_Beta_Unify $
+		Error_Unify_Const_mismatch
+		 (TypeVT $ tyFun @_ @'[])
+		 (TypeVT $ tyBool @_ @'[]))
+	 ]
+ ]
+
+-- * Class 'Sym_Bool_Vars'
+-- | A few boolean variables.
+class Sym_Bool_Vars repr where
+	x :: repr Bool
+	y :: repr Bool
+	z :: repr Bool
+instance Sym_Bool_Vars View where
+	x = View $ \_p _v -> "x"
+	y = View $ \_p _v -> "y"
+	z = View $ \_p _v -> "z"
+{-
+instance -- Trans_Boo_Const
+ ( Sym_Bool repr
+ , Sym_Bool_Vars repr
+ ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
+	x = trans_lift x
+	y = trans_lift y
+	z = trans_lift z
+-}
+
+-- * EDSL tests
+te1 = bool True && bool False
+te2 = (bool True && bool False) ||  (bool True && bool True)
+te3 = (bool True ||  bool False) && (bool True ||  bool True)
+te4 = bool True && not (bool False)
+te5 = bool True && not x
+te6 = x `xor` y
+te7 = (x `xor` y) `xor` z
+te8 = x `xor` (y `xor` bool True)
diff --git a/test/HUnit/Foldable.hs b/test/HUnit/Foldable.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Foldable.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Foldable where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy (->)
+ , Proxy Int
+ , Proxy Integer
+ , Proxy []
+ , Proxy ()
+ , Proxy (,)
+ , Proxy Foldable
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Foldable"
+ [ {-"[]" ==> Right (tyList (tyVar "a" varZ), [], "[]")
+ ,-} "[1, 2, 3]" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")
+ , "1 : 2 : 3 : []" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")
+ , "foldMap (\\(x0:Integer) -> [x0, x0]) [1, 2, 3]" ==> Right
+	 ( tyList tyInteger
+	 , [1, 1, 2, 2, 3, 3]
+	 , "foldMap (\\x0 -> x0 : x0 : []) (1 : 2 : 3 : [])" )
+ ]
diff --git a/test/HUnit/Functor.hs b/test/HUnit/Functor.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Functor.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Functor where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+
+import Language.Symantic ()
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy (->)
+ , Proxy Bool
+ , Proxy Functor
+ , Proxy Integer
+ , Proxy Maybe
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Functor"
+ [ "fmap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")
+ , "not `fmap` Just True" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")
+ , "not <$> Just True"    ==> Right (tyMaybe tyBool, Just False, "(\\x0 -> not x0) <$> Just True")
+ , "False <$ Just True"   ==> Right (tyMaybe tyBool, Just False, "False <$ Just True")
+ ]
diff --git a/test/HUnit/Map.hs b/test/HUnit/Map.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Map.hs
@@ -0,0 +1,42 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Map where
+
+import Test.Tasty
+import Data.Map.Strict (Map)
+import Data.Proxy (Proxy(..))
+import Data.Text as Text
+import qualified Data.Map.Strict as Map
+
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy (->)
+ , Proxy []
+ , Proxy Int
+ , Proxy Integer
+ , Proxy Map
+ , Proxy Char
+ , Proxy (,)
+ , Proxy Num
+ , Proxy Monoid
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Map"
+ [ "Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c'])" ==> Right
+	 ( tyMap tyInteger tyChar
+	 , Map.fromList [(1, 'a'), (2, 'b'), (3, 'c')]
+	 , "Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : []))" )
+ , Text.concat
+	[ "Map.foldrWithKey"
+	, " (\\(k:Integer) (v:Char) (acc:(Integer,[Char])) ->"
+	, "  (k + fst acc, v : snd acc))"
+	, " (0, [])"
+	, " (Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c']))"
+	] ==> Right
+	 ( tyInteger `tyTuple2` tyString
+	 , (6, "abc")
+	 , "Map.foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, x1 : snd x2)))) (0, []) (Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : [])))" )
+ ]
diff --git a/test/HUnit/MonoFunctor.hs b/test/HUnit/MonoFunctor.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/MonoFunctor.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.MonoFunctor where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+import qualified Data.MonoTraversable as MT
+
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy (->)
+ , Proxy []
+ , Proxy Integer
+ , Proxy Bool
+ , Proxy Char
+ , Proxy MT.MonoFunctor
+ , Proxy Maybe
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "MonoFunctor"
+ [ "omap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "omap (\\x0 -> not x0) (Just True)")
+ , "omap Char.toUpper ['a', 'b', 'c']" ==> Right (tyList tyChar, "ABC", "omap (\\x0 -> Char.toUpper x0) ('a' : 'b' : 'c' : [])" )
+ ]
diff --git a/test/HUnit/Num.hs b/test/HUnit/Num.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Num.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module HUnit.Num where
+
+import Test.Tasty
+import Prelude (Num)
+import Prelude hiding (Num(..))
+
+import Language.Symantic
+import Language.Symantic.Lib
+import Testing.Compiling
+
+-- * Tests
+type SS =
+ [ Proxy (->)
+ , Proxy Integer
+ , Proxy Num
+ , Proxy Num2
+ , Proxy Int
+ , Proxy Integral
+ , Proxy Foldable
+ , Proxy Traversable
+ , Proxy []
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Num"
+ [ "42"                        ==> Right (tyInteger,  42, "42")
+ , "-42"                       ==> Right (tyInteger, -42, "negate 42")
+ , "- -42"                     ==> Right (tyInteger,  42, "negate (negate 42)")
+ , "1 + -2"                    ==> Right (tyInteger,  -1, "1 + negate 2")
+ , "-1 + -2"                   ==> Right (tyInteger,  -3, "negate 1 + negate 2")
+ , "-(1 + -2)"                 ==> Right (tyInteger,   1, "negate (1 + negate 2)")
+ , "(+) 1 2"                   ==> Right (tyInteger,   3, "1 + 2")
+ , "1+2"                       ==> Right (tyInteger,   3, "1 + 2")
+ , "1 +2"                      ==> Right (tyInteger,   3, "1 + 2")
+ , "1+ 2"                      ==> Right (tyInteger,   3, "1 + 2")
+ , "1 + 2"                     ==> Right (tyInteger,   3, "1 + 2")
+ , "1 + 2 - 3"                 ==> Right (tyInteger,   0, "1 + 2 - 3")
+ , "1 + 2 * 3"                 ==> Right (tyInteger,   7, "1 + 2 * 3")
+ , "3 * 2 + 1"                 ==> Right (tyInteger,   7, "3 * 2 + 1")
+ , "3 * (2 + 1)"               ==> Right (tyInteger,   9, "3 * (2 + 1)")
+ , "4 + 3 * 2 + 1"             ==> Right (tyInteger,  11, "4 + 3 * 2 + 1")
+ , "5 * 4 + 3 * 2 + 1"         ==> Right (tyInteger,  27, "5 * 4 + 3 * 2 + 1")
+ , "negate`42"                 ==> Right (tyInteger, -42, "negate 42")
+ , "42`negate"                 ==> Right (tyInteger, -42, "negate 42")
+ , "42`negate "                ==> Right (tyInteger, -42, "negate 42")
+ , "42`negate`negate"          ==> Right (tyInteger,  42, "negate (negate 42)")
+ , "42`abs`negate"             ==> Right (tyInteger, -42, "negate (abs 42)")
+ , "42`negate`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")
+ , "abs`negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")
+ , "negate`abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")
+ , "negate`abs`42`mod`9"       ==> Right (tyInteger,   3, "negate (abs 42) `mod` 9")
+ , "negate abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")
+ , "negate 42`abs"             ==> Right (tyInteger, -42, "negate (abs 42)")
+ , "(+) negate`2 44"           ==> Right (tyInteger,  42, "negate 2 + 44")
+ , "(+) 2`negate 44"           ==> Right (tyInteger,  42, "negate 2 + 44")
+ , "(+) (negate`2) 44"         ==> Right (tyInteger,  42, "negate 2 + 44")
+ , "abs negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")
+ , "(+) 40 2"                  ==> Right (tyInteger,  42, "40 + 2")
+ , "(+) 40 $ -2"               ==> Right (tyInteger,  38, "(($) (\\x0 -> 40 + x0)) (negate 2)")
+ , "negate 42 + 42`negate"     ==> Right (tyInteger, -84, "negate 42 + negate 42")
+ , "(+) (negate 42) 42`negate" ==> Right (tyInteger, -84, "negate 42 + negate 42")
+ , "(+) negate`42 42`negate"   ==> Right (tyInteger, -84, "negate 42 + negate 42")
+ , "42`abs`negate`mod`abs`negate`9" ==> Right (tyInteger, 3, "negate (abs 42) `mod` abs (negate 9)")
+ , "abs`42`negate"             ==> Right (tyInteger,  42, "abs (negate 42)")
+ , "negate`42`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")
+ , testGroup "Error_Term"
+   [ "(+) 40 -2"  ==> Left (tyInteger,
+		Right $ Error_Term_Beta $ Error_Beta_Unify $
+		Error_Unify_Const_mismatch
+		 (TypeVT $ tyFun @_ @'[])
+		 (TypeVT $ tyInteger @_ @'[]))
+	 , "(+) 40 - 2" ==> Left (tyInteger,
+		Right $ Error_Term_Beta $ Error_Beta_Unify $
+		Error_Unify_Const_mismatch
+		 (TypeVT $ tyFun @_ @'[])
+		 (TypeVT $ tyInteger @_ @'[]))
+	 ]
+ ]
+
+-- | A newtype to test prefix and postfix.
+newtype Num2 a = Num2 a
+type instance Sym Num2 = Sym_Num2
+class Sym_Num2 (term:: * -> *) where
+
+instance Sym_Num2 Eval where
+instance Sym_Num2 View where
+instance Sym_Num2 (Dup r1 r2) where
+instance Sym_Num2 term => Sym_Num2 (BetaT term) where
+instance NameTyOf Num2 where
+	nameTyOf _c = ["Num2"] `Mod` "Num2"
+instance FixityOf Num2
+instance ClassInstancesFor Num2
+instance TypeInstancesFor Num2
+instance Gram_Term_AtomsFor src ss g Num2
+instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where
+	moduleFor = ["Num2"] `moduleWhere`
+	 [ "abs"    `withPrefix`   9 := teNum_abs
+	 , "negate" `withPrefix`  10 := teNum_negate
+	 , "abs"    `withPostfix`  9 := teNum_abs
+	 , "negate" `withPostfix` 10 := teNum_negate
+	 ]
diff --git a/test/HUnit/Tuple2.hs b/test/HUnit/Tuple2.hs
new file mode 100644
--- /dev/null
+++ b/test/HUnit/Tuple2.hs
@@ -0,0 +1,27 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module HUnit.Tuple2 where
+
+import Test.Tasty
+import Data.Proxy (Proxy(..))
+
+import Language.Symantic.Lib
+import Testing.Compiling
+
+type SS =
+ [ Proxy (->)
+ , Proxy Integer
+ , Proxy ()
+ , Proxy (,)
+ ]
+(==>) = readTe @() @SS
+
+hunits :: TestTree
+hunits = testGroup "Tuple2"
+ [ "()"             ==> Right (tyUnit, (), "()")
+ , "(,) 1 2"        ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")
+ , "(1,2)"          ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")
+ , "((1,2), (3,4))" ==> Right
+	 ( let t = tyTuple2 tyInteger tyInteger in tyTuple2 t t
+	 , ((1,2),(3,4))
+	 , "((1, 2), (3, 4))" )
+ ]
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,15 @@
+module Main where
+
+import Test.Tasty
+
+import Golden
+import HUnit
+
+main :: IO ()
+main = do
+	goldens <- goldensIO
+	defaultMain $
+		testGroup "Symantic"
+		 [ goldens
+		 , hunits
+		 ]
diff --git a/test/Testing/Compiling.hs b/test/Testing/Compiling.hs
new file mode 100644
--- /dev/null
+++ b/test/Testing/Compiling.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Testing.Compiling where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+import Debug.Trace (trace)
+
+import Control.Arrow (left)
+import Data.Functor.Identity (Identity(..))
+import Data.Text (Text)
+import Data.Type.Equality
+import Data.Void (Void)
+import qualified Control.Monad.Classes.Run as MC
+import qualified Control.Monad.Trans.State.Strict as S
+import qualified Data.List as List
+import qualified Data.Text as Text
+import qualified Text.Megaparsec as P
+
+import Language.Symantic.Grammar
+import Language.Symantic
+import Language.Symantic.Lib ()
+
+import Testing.Megaparsec ()
+
+type G src ss =
+ P.ParsecT Void Text
+           (S.StateT (Imports NameTe, Modules src ss)
+                     ((S.StateT (Imports NameTy, ModulesTy src))
+                                Identity))
+
+parseTe ::
+ forall ss src.
+ ImportTypes ss =>
+ ModulesTyInj ss =>
+ ModulesInj src ss =>
+ Gram_Term src ss (G src ss) =>
+ Text -> Either (P.ParseError Char Void) (AST_Term src ss)
+parseTe inp =
+	let modsTe :: Modules src ss = either (error . show) id modulesInj in
+	let impsTe = [] `importModules` modsTe in
+	let modsTy = modulesTyInj @ss @src in
+	let impsTy = importTypes @ss [] in
+	runIdentity $
+	MC.evalStateStrict (impsTy, modsTy) $
+	MC.evalStateStrict (impsTe, modsTe) $
+	P.runParserT g "" inp
+	where g = unCF $ g_term <* eoi
+
+readTe ::
+ forall src ss t.
+ ( Eq t
+ , Eq src
+ , Gram_Term src ss (G src ss)
+ , ImportTypes ss
+ , ModulesInj src ss
+ , ModulesTyInj ss
+ , Show src
+ , Show t
+ , SourceInj (AST_Type src) src
+ , SourceInj (KindK src) src
+ , SourceInj (TypeT src '[]) src
+ , SourceInj (TypeVT src) src
+ , Syms ss (BetaT View)
+ , Syms ss Eval
+ , Syms ss View
+ ) =>
+ Text ->
+ Either ( Type src '[] t
+        , Either (P.ParseError Char Void)
+                 (Error_Term src) )
+        (Type src '[] t, t, Text) ->
+ TestTree
+readTe inp expected =
+	testCase (elide inp) $
+	case reduceTeApp <$> parseTe @ss inp of
+	 Left err -> Left (Left err) @?= snd `left` expected
+	 Right ast ->
+		case readTerm CtxTyZ ast of
+		 Left err -> Left (Right err) @?= snd `left` expected
+		 Right term ->
+			case term of
+			 TermVT (Term q t (TeSym te)) ->
+				case expected of
+				 Left (_, err) -> Right ("…"::Text) @?= Left err
+				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->
+					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
+					case lenVars t of
+					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
+					 LenZ ->
+						case proveConstraint q of
+						 Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
+						 Just Dict ->
+							case t `eqType` ty_expected of
+							 Nothing -> return $ Left $ Right $
+								Error_Term_Beta $ Error_Beta_Unify $
+								Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
+							 Just Refl ->
+								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
+
+maybeRight :: Either l r -> Maybe r
+maybeRight (Right r) = Just r
+maybeRight Left{}    = Nothing
+
+elide :: Text -> String
+elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
+elide s = Text.unpack s
+
+dbg :: Show a => String -> a -> a
+dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x
diff --git a/test/Testing/Megaparsec.hs b/test/Testing/Megaparsec.hs
new file mode 100644
--- /dev/null
+++ b/test/Testing/Megaparsec.hs
@@ -0,0 +1,181 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Symantic instances for Megaparsec
+module Testing.Megaparsec where
+
+import Control.Applicative (Applicative(..))
+import Control.Monad (Monad(..))
+import Data.Char (Char)
+import Data.Either (Either(..))
+import Data.Function (($), (.))
+import Data.Functor (Functor(..), (<$>))
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Ord (Ord(..))
+import Data.String (IsString(..))
+import Data.Typeable ()
+import Text.Show (Show(..))
+import qualified Control.Applicative as Alt
+import qualified Control.Monad.Classes as MC
+import qualified Data.Char as Char
+import qualified Data.Text as Text
+import qualified Data.Text.Lazy as TL
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
+
+import Language.Symantic.Grammar as Sym
+import qualified Language.Symantic as Sym
+import Language.Symantic.Lib ()
+
+-- * Type 'ParsecC'
+-- | Convenient alias for defining instances involving 'P.ParsecT'.
+type ParsecC e s = (P.Token s ~ Char, P.Stream s, Ord e)
+instance ParsecC e [Char] => IsString (P.ParsecT e [Char] m [Char]) where
+	fromString = P.string
+
+--
+-- Readers
+--
+
+-- NonEmpty P.SourcePos
+instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where
+	askBefore g = do
+		s <- P.statePos <$> P.getParserState
+		($ s) <$> g
+	askAfter g = do
+		f <- g
+		f . P.statePos <$> P.getParserState
+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True
+instance ParsecC e s => MC.MonadReaderN 'MC.Zero (NonEmpty P.SourcePos) (P.ParsecT e s m) where
+	askN _n = P.statePos <$> P.getParserState
+-- P.SourcePos
+instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where
+	askBefore g = do
+		s <- P.getPosition
+		($ s) <$> g
+	askAfter g = do
+		f <- g
+		f <$> P.getPosition
+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True
+instance ParsecC e s => MC.MonadReaderN 'MC.Zero P.SourcePos (P.ParsecT e s m) where
+	askN _n = P.getPosition
+-- ()
+instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where
+	askBefore = fmap ($ ())
+	askAfter  = fmap ($ ())
+
+--
+-- States
+--
+
+-- st
+type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False
+instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where
+	stateBefore g = do
+		s <- MC.get
+		f <- g
+		let (s', a) = f s
+		MC.put s'
+		return a
+	stateAfter g = do
+		f <- g
+		s <- MC.get
+		let (s_, a) = f s
+		MC.put s_
+		return a
+	getBefore g = do
+		s <- MC.get
+		f <- g
+		return (f s)
+	getAfter g = do
+		f <- g
+		s <- MC.get
+		return (f s)
+	put g = do
+		(s, a) <- g
+		MC.put s
+		return a
+
+--
+-- Sym instances
+--
+instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where
+	catch me {- if you can :-} = do
+		e <- me
+		case e of
+		 Left err -> fail $ show err
+		 Right a -> return a
+instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where
+	rule = P.label . Text.unpack
+instance ParsecC e s => Sym.Gram_Char (P.ParsecT e s m) where
+	any          = P.anyChar
+	eoi          = P.eof
+	char         = P.char
+	unicat cat   = P.satisfy $ (`elem` cats) . Char.generalCategory
+		where cats = unicode_categories cat
+	range (l, h) = P.satisfy $ \c -> l <= c && c <= h
+	Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f
+instance ParsecC e String => Sym.Gram_String (P.ParsecT e String m) where
+	string = P.string
+instance ParsecC e Text.Text => Sym.Gram_String (P.ParsecT e Text.Text m) where
+	string t   = Text.unpack <$> P.string (Text.pack t)
+	text       = P.string
+	textLazy t = TL.fromStrict <$> P.string (TL.toStrict t)
+instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where
+	empty  = Alt.empty
+	(<+>)  = (Alt.<|>)
+	choice = P.choice
+instance ParsecC e s => Sym.Gram_Try (P.ParsecT e s m) where
+	try = P.try
+instance ParsecC e s => Sym.Gram_RegR (P.ParsecT e s m) where
+	Terminal f .*> Reg x = Reg $ f <*> x
+instance ParsecC e s => Sym.Gram_RegL (P.ParsecT e s m) where
+	Reg f <*. Terminal x = Reg $ f <*> x
+instance ParsecC e s => Sym.Gram_App (P.ParsecT e s m) where
+	between = P.between
+instance ParsecC e s => Sym.Gram_AltApp (P.ParsecT e s m) where
+	option   = P.option
+	optional = P.optional
+	many     = P.many
+	some     = P.some
+	manySkip = P.skipMany
+instance ParsecC e s => Sym.Gram_CF (P.ParsecT e s m) where
+	CF f <& Reg p        = CF $ P.lookAhead f <*> p
+	Reg f &> CF p        = CF $ P.lookAhead f <*> p
+	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Comment (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Op (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Mod (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Type_Name (P.ParsecT e s m)
+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Term_Name (P.ParsecT e s m)
+instance -- Sym.Gram_Type
+ ( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
+ , Gram_Source src (P.ParsecT e s m)
+ , Show src
+ , MC.MonadState ( Sym.Imports Sym.NameTy
+                 , Sym.ModulesTy src )
+                 (P.ParsecT e s m)
+ ) => Sym.Gram_Type src (P.ParsecT e s m)
+instance -- Sym.Gram_Term_Type
+ ( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
+ , Show src
+ , MC.MonadState ( Sym.Imports Sym.NameTy
+                 , Sym.ModulesTy src )
+                 (P.ParsecT e s m)
+ , Gram_Source src           (P.ParsecT e s m)
+ ) => Sym.Gram_Term_Type src (P.ParsecT e s m)
+instance -- Sym.Gram_Term
+ ( ParsecC e s
+ , Sym.Gram_String (P.ParsecT e s m)
+ , Show src
+ , MC.MonadState ( Sym.Imports Sym.NameTy
+                 , Sym.ModulesTy src )
+                 (P.ParsecT e s m)
+ , MC.MonadState ( Sym.Imports Sym.NameTe
+                 , Sym.Modules src ss )
+                 (P.ParsecT e s m)
+ , Sym.Gram_Source src        (P.ParsecT e s m)
+ , Sym.Gram_Term_Atoms src ss (P.ParsecT e s m)
+ ) => Sym.Gram_Term src ss    (P.ParsecT e s m)