From 111350d915ce1dbd55bb386956c61f42c8d097e0 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm+symantic@autogeree.net>
Date: Sun, 23 Oct 2016 16:36:22 +0200
Subject: [PATCH] init

---
 Language/Symantic/AST/Test.hs              |  27 +++-
 Language/Symantic/Expr/Applicative.hs      |  12 +-
 Language/Symantic/Expr/Applicative/Test.hs |   1 +
 Language/Symantic/Expr/Bool/Test.hs        |   6 +-
 Language/Symantic/Expr/Common.hs           |  29 ++--
 Language/Symantic/Expr/Functor.hs          |   5 +-
 Language/Symantic/Expr/Int/Test.hs         |   6 +-
 Language/Symantic/Expr/Lambda.hs           |  10 +-
 Language/Symantic/Expr/List.hs             |  10 +-
 Language/Symantic/Expr/Map.hs              |  10 +-
 Language/Symantic/Expr/Maybe.hs            |  10 +-
 Language/Symantic/Expr/Tuple.hs            |   8 +-
 Language/Symantic/Lib/Data/Peano.hs        |  27 ++--
 Language/Symantic/Repr/Dup.hs              |   6 +
 Language/Symantic/Type/Bool.hs             |   9 +-
 Language/Symantic/Type/Common.hs           | 157 ++++++++++++++-------
 Language/Symantic/Type/Fun.hs              |  25 +++-
 Language/Symantic/Type/Int.hs              |   9 +-
 Language/Symantic/Type/List.hs             |  21 ++-
 Language/Symantic/Type/Map.hs              |  23 ++-
 Language/Symantic/Type/Maybe.hs            |  21 ++-
 Language/Symantic/Type/Ordering.hs         |   9 +-
 Language/Symantic/Type/Tuple.hs            |  22 +--
 Language/Symantic/Type/Unit.hs             |   9 +-
 Language/Symantic/Type/Var.hs              |  77 ++++++++--
 25 files changed, 379 insertions(+), 170 deletions(-)

diff --git a/Language/Symantic/AST/Test.hs b/Language/Symantic/AST/Test.hs
index 551d2fb..9024651 100644
--- a/Language/Symantic/AST/Test.hs
+++ b/Language/Symantic/AST/Test.hs
@@ -162,10 +162,17 @@ op2_from_AST op ty_lit asts ex ast ctx k =
 	 _ -> Left $ error_expr ex $
 		Error_Expr_Wrong_number_of_arguments ast 2
 
-instance -- Type_from AST Type_Var
+instance -- Type_from AST Type_Var0
  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
- , Implicit_HBool (Is_Last_Type (Type_Var root) root)
- ) => Type_from AST (Type_Var root) where
+ , Implicit_HBool (Is_Last_Type (Type_Var0 root) root)
+ ) => Type_from AST (Type_Var0 root) where
+	type_from ty ast _k =
+		Left $ error_type_unsupported ty ast
+	 -- NOTE: no support so far.
+instance -- Type_from AST Type_Var1
+ ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
+ , Implicit_HBool (Is_Last_Type (Type_Var1 root) root)
+ ) => Type_from AST (Type_Var1 root) where
 	type_from ty ast _k =
 		Left $ error_type_unsupported ty ast
 	 -- NOTE: no support so far.
@@ -276,6 +283,7 @@ instance -- Type_from AST Type_List
 			 _ -> Left $ lift_error_type $
 				Error_Type_Wrong_number_of_arguments ast 1
 		 _ -> Left $ error_type_unsupported ty ast
+
 instance -- Type1_from AST Type_Bool
  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
  , Implicit_HBool (Is_Last_Type (Type_Bool root) root)
@@ -292,10 +300,14 @@ instance -- Type1_from AST Type_Ordering
  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
  , Implicit_HBool (Is_Last_Type (Type_Ordering root) root)
  ) => Type1_from AST (Type_Ordering root)
-instance -- Type1_from AST Type_Var
+instance -- Type1_from AST Type_Var0
+ ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
+ , Implicit_HBool (Is_Last_Type (Type_Var0 root) root)
+ ) => Type1_from AST (Type_Var0 root)
+instance -- Type1_from AST Type_Var1
  ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
- , Implicit_HBool (Is_Last_Type (Type_Var root) root)
- ) => Type1_from AST (Type_Var root)
+ , Implicit_HBool (Is_Last_Type (Type_Var1 root) root)
+ ) => Type1_from AST (Type_Var1 root)
 instance -- Type1_from AST Type_Maybe
  ( Type_from AST root
  , Lift_Type_Root Type_Maybe root
@@ -349,6 +361,7 @@ instance -- Type1_from AST Type_Fun
 			 _ -> Left $ lift_error_type $
 				Error_Type_Wrong_number_of_arguments ast 1
 		 _ -> Left $ error_type_unsupported ty ast
+
 instance -- Expr_from AST Expr_Bool
  ( Eq_Type (Type_Root_of_Expr root)
  , Type_from AST (Type_Root_of_Expr root)
@@ -554,6 +567,7 @@ instance -- Expr_from AST Expr_Functor
  , Type_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , String_from_Type (Type_Root_of_Expr root)
+ -- , Lift_Type   Type_Var1      (Type_of_Expr root)
  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  , Unlift_Type1 (Type_of_Expr root)
@@ -572,6 +586,7 @@ instance -- Expr_from AST Expr_Applicative
  , Type1_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , String_from_Type (Type_Root_of_Expr root)
+ -- , Lift_Type   Type_Var1      (Type_of_Expr root)
  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  , Eq_Type1 (Type_Root_of_Expr root)
diff --git a/Language/Symantic/Expr/Applicative.hs b/Language/Symantic/Expr/Applicative.hs
index 3444647..f8c7b57 100644
--- a/Language/Symantic/Expr/Applicative.hs
+++ b/Language/Symantic/Expr/Applicative.hs
@@ -51,9 +51,13 @@ infixl 4 <*>
 -- NOTE: see comment of 'Functor_with_Lambda'.
 class    (Applicative f, Traversable f) => Applicative_with_Lambda f
 instance (Applicative f, Traversable f) => Applicative_with_Lambda f
-instance Constraint_Type1 Applicative_with_Lambda (Type_Type1 t1 root)
-instance Constraint_Type1 Applicative_with_Lambda (Type_Type2 c2 t2 root)
-instance Constraint_Type1 Applicative_with_Lambda (Type_Var root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Bool     root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Fun lam  root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Int      root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Ordering root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Unit     root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Var0     root)
+instance Constraint_Type1 Applicative_with_Lambda (Type_Var1     root)
 
 -- * Type 'Expr_Applicative'
 -- | Expression.
@@ -112,7 +116,7 @@ ltstargt_from ast_fg ast_fa ex ast ctx k =
 	check_type1 ex ast ty_fg $ \(Type_Type1 _f (ty_g::Type_Root_of_Expr root h_g), _) ->
 	check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 ty_f) ->
 	check_eq_type1 ex ast ty_fg ty_fa $ \Refl ->
-	check_type_fun ex ast ty_g $ \(ty_g_a `Type_Fun` ty_g_b
+	check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
 	 :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
 	check_constraint1_type ex (Proxy::Proxy Applicative_with_Lambda) ast ty_fa $ \Dict ->
 	check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
diff --git a/Language/Symantic/Expr/Applicative/Test.hs b/Language/Symantic/Expr/Applicative/Test.hs
index a66cefb..f97de93 100644
--- a/Language/Symantic/Expr/Applicative/Test.hs
+++ b/Language/Symantic/Expr/Applicative/Test.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ScopedTypeVariables #-}
diff --git a/Language/Symantic/Expr/Bool/Test.hs b/Language/Symantic/Expr/Bool/Test.hs
index d230541..acd8d6c 100644
--- a/Language/Symantic/Expr/Bool/Test.hs
+++ b/Language/Symantic/Expr/Bool/Test.hs
@@ -116,9 +116,9 @@ tests = testGroup "Bool" $
 	 ] in ast ==> Left (Proxy::Proxy Bool,
 	Error_Expr_Alt_Curr $
 	Error_Expr_Type_mismatch ast
-	 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-	 ::Type_Root (Type_Var :|: Type_Fun IO :|: Type_Bool)
-	             (Lambda IO Zero (Succ Zero))))
+	 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
+	 ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun IO :|: Type_Bool)
+	             (Lambda IO Var0 Var0)))
 	 (Exists_Type type_bool))
  , AST "app"
 	 [ AST "val"
diff --git a/Language/Symantic/Expr/Common.hs b/Language/Symantic/Expr/Common.hs
index 9ae55d2..8f55213 100644
--- a/Language/Symantic/Expr/Common.hs
+++ b/Language/Symantic/Expr/Common.hs
@@ -12,11 +12,12 @@
 {-# LANGUAGE UndecidableInstances #-}
 module Language.Symantic.Expr.Common where
 
+import Data.Maybe (fromMaybe)
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
-import qualified Data.Text as Text
 import Data.Type.Equality ((:~:)(Refl))
 import GHC.Prim (Constraint)
+import qualified Data.Text as Text
 
 import Language.Symantic.Type
 
@@ -195,7 +196,7 @@ type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 -- NOTE: include 'Type_Var' only to use it
 -- within 'Error_Expr_Type_mismatch' so far.
 type Type_Root_of_Expr (ex:: *)
- =   Type_Root (Type_Var :|: Type_of_Expr (Root_of_Expr ex))
+ =   Type_Root (Type_Var0 :|: Type_Var1 :|: Type_of_Expr (Root_of_Expr ex))
 
 -- * Type 'Expr_Root'
 -- | The root expression, passing itself as parameter to the given expression.
@@ -595,7 +596,7 @@ check_constraint1_type ex c ast ty k =
 		Error_Expr_Constraint_missing ast
 		 (Exists_Type ty)
 
--- | Parsing utility to check that the given type is a 'Type_Maybe'
+-- | Parsing utility to check that the given type is a 'Type_Type1'
 -- or raise 'Error_Expr_Type_mismatch'.
 check_type1
  :: forall ast ex root ty h ret.
@@ -607,27 +608,19 @@ check_type1
                    (Error_of_Expr ast root)
  )
  => Proxy ex -> ast -> ty h
- -> (forall (f:: * -> *).
-     ( Type_Type1 f ty h
-     , Lift_Type1 f (Type_Var :|: Type_of_Expr root)
+ -> (forall (t1:: *).
+     ( Type_Type1 t1 ty h
+     , Lift_Type1 t1 (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
      ) -> Either (Error_of_Expr ast root) ret)
  -> Either (Error_of_Expr ast root) ret
 check_type1 ex ast ty k =
-	case unlift_type1 (unType_Root ty) $ Just . k of
-	 Just x -> x
-	 Nothing -> undefined
-		{-
-	 Just x -> k x
-	 Nothing ->
-		error ("check_type1: " ++ show ty)
-		Left $
+	(`fromMaybe` unlift_type1 (unType_Root ty) (Just . k)) $
+	Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (lift_type_root (Type_Type1 $ type_var SZero) -- $ type_var SZero
-		 :: Type_Root_of_Expr ex (Zero1 Zero)))
+		 (Exists_Type (type_var1 SZero (type_var0 SZero)
+		 :: Type_Root_of_Expr ex (Var1 Var0)))
 		 (Exists_Type ty)
-		-}
-data Zero1 a
 
 -- * Type 'Error_Read'
 -- | Error parsing a host-term.
diff --git a/Language/Symantic/Expr/Functor.hs b/Language/Symantic/Expr/Functor.hs
index 236cd11..6837a8e 100644
--- a/Language/Symantic/Expr/Functor.hs
+++ b/Language/Symantic/Expr/Functor.hs
@@ -63,7 +63,8 @@ instance Constraint_Type1 Functor_with_Lambda (Type_Bool     root)
 instance Constraint_Type1 Functor_with_Lambda (Type_Int      root)
 instance Constraint_Type1 Functor_with_Lambda (Type_Ordering root)
 instance Constraint_Type1 Functor_with_Lambda (Type_Unit     root)
-instance Constraint_Type1 Functor_with_Lambda (Type_Var      root)
+instance Constraint_Type1 Functor_with_Lambda (Type_Var0     root)
+instance Constraint_Type1 Functor_with_Lambda (Type_Var1     root)
 
 -- * Type 'Expr_Functor'
 -- | Expression.
@@ -95,7 +96,7 @@ fmap_from ast_g ast_fa ex ast ctx k =
 	 \(ty_g::Type_Root_of_Expr root h_g) (Forall_Repr_with_Context g) ->
 	expr_from (Proxy::Proxy root) ast_fa ctx $
 	 \(ty_fa::Type_Root_of_Expr root h_fa) (Forall_Repr_with_Context fa) ->
-	check_type_fun ex ast ty_g $ \(ty_g_a `Type_Fun` ty_g_b
+	check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
 	 :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
 	check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 f_lift) ->
 	check_constraint1_type ex (Proxy::Proxy Functor_with_Lambda) ast ty_fa $ \Dict ->
diff --git a/Language/Symantic/Expr/Int/Test.hs b/Language/Symantic/Expr/Int/Test.hs
index 2275589..58b3094 100644
--- a/Language/Symantic/Expr/Int/Test.hs
+++ b/Language/Symantic/Expr/Int/Test.hs
@@ -98,9 +98,9 @@ tests = testGroup "Int" $
 	 ] in ast ==> Left (Proxy::Proxy Int,
 	Error_Expr_Alt_Curr $
 	Error_Expr_Type_mismatch ast
-	 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-	 ::Type_Root (Type_Var :|: Type_Fun IO :|: Type_Int)
-	             (Lambda IO Zero (Succ Zero))))
+	 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
+	 ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun IO :|: Type_Int)
+	             (Lambda IO Var0 Var0)))
 	 (Exists_Type type_int))
  , AST "app"
 	 [ AST "val"
diff --git a/Language/Symantic/Expr/Lambda.hs b/Language/Symantic/Expr/Lambda.hs
index 86423ca..b1a9623 100644
--- a/Language/Symantic/Expr/Lambda.hs
+++ b/Language/Symantic/Expr/Lambda.hs
@@ -114,8 +114,8 @@ check_type_fun ex ast ty k =
 	 Nothing -> Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-		 :: Type_Root_of_Expr ex (Lambda lam Zero (Succ Zero))))
+		 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
+		 :: Type_Root_of_Expr ex (Lambda lam Var0 Var0)))
 		 (Exists_Type ty)
 
 -- | Parse a /lambda variable/.
@@ -170,10 +170,10 @@ app_from ast_lam ast_arg_actual ex ast ctx k =
 		 Nothing -> Left $
 			error_expr ex $
 			Error_Expr_Type_mismatch ast
-			 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-			 :: Type_Root_of_Expr (Expr_Lambda lam root) (Lambda lam Zero (Succ Zero))))
+			 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
+			 :: Type_Root_of_Expr (Expr_Lambda lam root) (Lambda lam Var0 Var0)))
 			 (Exists_Type ty_lam)
-		 Just (ty_arg_expected `Type_Fun` ty_res
+		 Just (Type_Type2 Proxy ty_arg_expected ty_res
 		  :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
 			check_eq_type ex ast
 			 ty_arg_expected ty_arg_actual $ \Refl ->
diff --git a/Language/Symantic/Expr/List.hs b/Language/Symantic/Expr/List.hs
index 73ad8a5..a08b3f7 100644
--- a/Language/Symantic/Expr/List.hs
+++ b/Language/Symantic/Expr/List.hs
@@ -54,9 +54,9 @@ type instance Type_of_Expr      (Expr_List lam root)      = Type_List
 type instance Sym_of_Expr       (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr)
 type instance Error_of_Expr ast (Expr_List lam root)      = No_Error_Expr
 
-instance Constraint_Type1 Functor_with_Lambda (Type_Type1 [] root) where
+instance Constraint_Type1 Functor_with_Lambda (Type_List root) where
 	constraint_type1 _c (Type_Type1 _ _) = Just Dict
-instance Constraint_Type1 Applicative_with_Lambda (Type_Type1 [] root) where
+instance Constraint_Type1 Applicative_with_Lambda (Type_List root) where
 	constraint_type1 _c (Type_Type1 _ _) = Just Dict
 
 -- | Parsing utility to check that the given type is a 'Type_List'
@@ -79,8 +79,8 @@ check_type_list ex ast ty k =
 	 Nothing -> Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (type_list $ type_var SZero
-		 :: Type_Root_of_Expr ex [Zero]))
+		 (Exists_Type (type_list $ type_var0 SZero
+		 :: Type_Root_of_Expr ex [Var0]))
 		 (Exists_Type ty)
 
 -- | Parse 'list_empty'.
@@ -182,7 +182,7 @@ list_filter_from ast_f ast_l ex ast ctx k =
 	 \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
 	expr_from (Proxy::Proxy root) ast_l ctx $
 	 \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
-	check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
+	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 	 :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
 	check_eq_type ex ast type_bool ty_f_b $ \Refl ->
 	check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
diff --git a/Language/Symantic/Expr/Map.hs b/Language/Symantic/Expr/Map.hs
index 756d511..7f3021f 100644
--- a/Language/Symantic/Expr/Map.hs
+++ b/Language/Symantic/Expr/Map.hs
@@ -60,8 +60,8 @@ check_type_map ex ast ty k =
 	 Nothing -> Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (type_map (type_var SZero) (type_var $ SSucc SZero)
-		 :: Type_Root_of_Expr ex (Map Zero (Succ Zero))))
+		 (Exists_Type (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
+		 :: Type_Root_of_Expr ex (Map Var0 Var0)))
 		 (Exists_Type ty)
 
 -- | Parse 'map_from_list'.
@@ -85,7 +85,7 @@ map_from_list_from ast_l ex ast ctx k =
 	expr_from (Proxy::Proxy root) ast_l ctx $
 	 \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
 	check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_t) ->
-	check_type_tuple2 ex ast ty_l_t $ \(Type_Tuple2 ty_k ty_a) ->
+	check_type_tuple2 ex ast ty_l_t $ \(Type_Type2 Proxy ty_k ty_a) ->
 	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 	k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
 	 \c -> map_from_list (l c)
@@ -112,9 +112,9 @@ map_map_from ast_f ast_m ex ast ctx k =
 	 \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
 	expr_from (Proxy::Proxy root) ast_m ctx $
 	 \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
-	check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
+	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
 	 :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
-	check_type_map ex ast ty_m $ \(Type_Map ty_m_k ty_m_a) ->
+	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 	check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
 	check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
 	k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
diff --git a/Language/Symantic/Expr/Maybe.hs b/Language/Symantic/Expr/Maybe.hs
index fb9a369..774b609 100644
--- a/Language/Symantic/Expr/Maybe.hs
+++ b/Language/Symantic/Expr/Maybe.hs
@@ -54,9 +54,9 @@ type instance Type_of_Expr      (Expr_Maybe lam root)      = Type_Maybe
 type instance Sym_of_Expr       (Expr_Maybe lam root) repr = (Sym_Maybe repr, Sym_Maybe_Lam lam repr)
 type instance Error_of_Expr ast (Expr_Maybe lam root)      = No_Error_Expr
 
-instance Constraint_Type1 Functor_with_Lambda (Type_Type1 Maybe root) where
+instance Constraint_Type1 Functor_with_Lambda (Type_Maybe root) where
 	constraint_type1 _c (Type_Type1 _ _) = Just Dict
-instance Constraint_Type1 Applicative_with_Lambda (Type_Type1 Maybe root) where
+instance Constraint_Type1 Applicative_with_Lambda (Type_Maybe root) where
 	constraint_type1 _c (Type_Type1 _ _) = Just Dict
 
 -- | Parsing utility to check that the given type is a 'Type_Maybe'
@@ -79,8 +79,8 @@ check_type_maybe ex ast ty k =
 	 Nothing -> Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (type_maybe $ type_var SZero
-		 :: Type_Root_of_Expr ex (Maybe Zero)))
+		 (Exists_Type (type_maybe $ type_var0 SZero
+		 :: Type_Root_of_Expr ex (Maybe Var0)))
 		 (Exists_Type ty)
 
 -- | Parse 'maybe'.
@@ -106,7 +106,7 @@ maybe_from ast_n ast_j ast_m ex ast ctx k =
 	 \(ty_j::Type_Root_of_Expr root h_j) (Forall_Repr_with_Context j) ->
 	expr_from (Proxy::Proxy root) ast_m ctx $
 	 \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
-	check_type_fun ex ast ty_j $ \(ty_j_a `Type_Fun` ty_j_b
+	check_type_fun ex ast ty_j $ \(Type_Type2 Proxy ty_j_a ty_j_b
 	 :: Type_Fun lam (Type_Root_of_Expr root) h_j) ->
 	check_type_maybe ex ast ty_m $ \(Type_Type1 _ ty_m_a) ->
 	check_eq_type ex ast ty_n   ty_j_b $ \Refl ->
diff --git a/Language/Symantic/Expr/Tuple.hs b/Language/Symantic/Expr/Tuple.hs
index 71da575..fbcf581 100644
--- a/Language/Symantic/Expr/Tuple.hs
+++ b/Language/Symantic/Expr/Tuple.hs
@@ -23,8 +23,8 @@ class Sym_Tuple2 repr where
 	default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
 	tuple2 = trans_map2 tuple2
 
-instance Constraint_Type1 Functor_with_Lambda (Type_Type1 ((,) fst) root) where
-	constraint_type1 _c (Type_Type1 _ _) = Just Dict
+instance Constraint_Type1 Functor_with_Lambda (Type_Type1 (Proxy ((,) fst)) root) where
+	constraint_type1 _c Type_Type1{} = Just Dict
 
 -- * Type 'Expr_Tuple2'
 -- | Expression.
@@ -54,8 +54,8 @@ check_type_tuple2 ex ast ty k =
 	 Nothing -> Left $
 		error_expr ex $
 		Error_Expr_Type_mismatch ast
-		 (Exists_Type (type_tuple2 (type_var SZero) (type_var $ SSucc SZero)
-		 :: Type_Root_of_Expr ex (Zero, Succ Zero)))
+		 (Exists_Type (type_tuple2 (type_var0 SZero) (type_var0 $ SSucc SZero)
+		 :: Type_Root_of_Expr ex (Var0, Var0)))
 		 (Exists_Type ty)
 
 -- | Parse 'tuple2'.
diff --git a/Language/Symantic/Lib/Data/Peano.hs b/Language/Symantic/Lib/Data/Peano.hs
index 49cf67c..aae31bb 100644
--- a/Language/Symantic/Lib/Data/Peano.hs
+++ b/Language/Symantic/Lib/Data/Peano.hs
@@ -10,22 +10,31 @@ import Data.Type.Equality ((:~:)(Refl))
 -- * Types 'Zero' and 'Succ'
 -- | Type-level peano numbers of kind '*'.
 data Zero
--- | Undefined instance required to build errors.
-instance Eq  Zero
--- | Undefined instance required to build errors.
-instance Ord Zero
 data Succ p
--- | Undefined instance required to build errors.
-instance Eq  (Succ p)
--- | Undefined instance required to build errors.
-instance Ord (Succ p)
 
 -- * Type 'SPeano'
--- | Singleton for peano numbers.
+-- | Singleton for 'Zero' and 'Succ'.
 data SPeano p where
  SZero :: SPeano Zero
  SSucc :: SPeano p -> SPeano (Succ p)
 
+-- * Type 'IPeano'
+-- | Implicit construction of 'SPeano'.
+class IPeano p where
+	ipeano :: SPeano p
+instance IPeano Zero where
+	ipeano = SZero
+instance IPeano p => IPeano (Succ p) where
+	ipeano = SSucc ipeano
+
+-- * Type 'EPeano'
+data EPeano where
+	EPeano :: SPeano p -> EPeano
+instance Eq EPeano where
+	EPeano x == EPeano y =
+		(integral_from_peano x::Integer) ==
+		 integral_from_peano y
+
 integral_from_peano :: Integral i => SPeano p -> i
 integral_from_peano SZero = 0
 integral_from_peano (SSucc x) = 1 + integral_from_peano x
diff --git a/Language/Symantic/Repr/Dup.hs b/Language/Symantic/Repr/Dup.hs
index 62ba232..9cd4c86 100644
--- a/Language/Symantic/Repr/Dup.hs
+++ b/Language/Symantic/Repr/Dup.hs
@@ -1,3 +1,7 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies #-}
 -- | Interpreter to duplicate the representation of an expression
 -- in order to evaluate it with different interpreters.
 --
@@ -8,6 +12,8 @@
 -- it is mainly here for the sake of curiosity.
 module Language.Symantic.Repr.Dup where
 
+import Data.Foldable (foldr)
+
 import Language.Symantic.Expr
 
 -- | Interpreter's data.
diff --git a/Language/Symantic/Type/Bool.hs b/Language/Symantic/Type/Bool.hs
index bd927a2..2b2a199 100644
--- a/Language/Symantic/Type/Bool.hs
+++ b/Language/Symantic/Type/Bool.hs
@@ -1,20 +1,25 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Bool where
 
+import Data.Proxy
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Bool'
 -- | The 'Bool' type.
-type Type_Bool = Type_Type0 Bool
+type Type_Bool = Type_Type0 (Proxy Bool)
+
+pattern Type_Bool :: Type_Bool root Bool
+pattern Type_Bool  = Type_Type0 Proxy
 
 instance -- String_from_Type
  String_from_Type (Type_Bool root) where
 	string_from_type _ = "Bool"
 
--- | Convenient alias to include a 'Type_Bool' within a type.
+-- | Inject 'Type_Bool' within a root type.
 type_bool :: Lift_Type_Root Type_Bool root => root Bool
 type_bool = type_type0
diff --git a/Language/Symantic/Type/Common.hs b/Language/Symantic/Type/Common.hs
index ac7b0ed..ccb47eb 100644
--- a/Language/Symantic/Type/Common.hs
+++ b/Language/Symantic/Type/Common.hs
@@ -294,33 +294,44 @@ instance -- String_from_Type
 	string_from_type (Type_Alt_Curr t) = string_from_type t
 	string_from_type (Type_Alt_Next t) = string_from_type t
 
+type family Host_of px :: *
+type instance Host_of (Proxy h0) = h0
+
 -- * Type 'Type_Type0'
-data Type_Type0 t0 (root:: * -> *) h where
-	Type_Type0 :: Proxy t0 -> Type_Type0 t0 root t0
+data Type_Type0 px (root:: * -> *) h where
+	Type_Type0 :: px -> Type_Type0 px root (Host_of px)
 
-type instance Root_of_Type      (Type_Type0 t0 root) = root
-type instance Error_of_Type ast (Type_Type0 t0 root) = No_Error_Type
+type instance Root_of_Type      (Type_Type0 px root) = root
+type instance Error_of_Type ast (Type_Type0 px root) = No_Error_Type
 
 instance -- Eq_Type
- Eq_Type (Type_Type0 t0 root) where
+ Eq_Type (Type_Type0 (Proxy h0) root) where
 	eq_type Type_Type0{} Type_Type0{} = Just Refl
+instance -- Eq_Type
+ Eq_Type (Type_Type0 EPeano root) where
+	eq_type (Type_Type0 p1)
+	        (Type_Type0 p2)
+	 | p1 == p2
+	 = Just Refl
+	eq_type _ _ = Nothing
 instance -- Eq
- Eq (Type_Type0 t0 root h) where
+ Eq_Type (Type_Type0 px root) =>
+ Eq (Type_Type0 px root h) where
 	x == y = isJust $ x `eq_type` y
 instance -- Show
- String_from_Type (Type_Type0 t0 root) =>
- Show (Type_Type0 t0 root h) where
+ String_from_Type (Type_Type0 (Proxy h0) root) =>
+ Show (Type_Type0 (Proxy h0) root h0) where
 	show = string_from_type
-instance Eq t0 => Constraint_Type Eq (Type_Type0 t0 root) where
+instance Eq h0 => Constraint_Type Eq (Type_Type0 (Proxy h0) root) where
 	constraint_type _c Type_Type0{} = Just Dict
-instance Ord t0 => Constraint_Type Ord (Type_Type0 t0 root) where
+instance Ord h0 => Constraint_Type Ord (Type_Type0 (Proxy h0) root) where
 	constraint_type _c Type_Type0{} = Just Dict
-instance Unlift_Type1 (Type_Type0 t0)
-instance Eq_Type1 (Type_Type0 t0 root)
+instance Unlift_Type1 (Type_Type0 px)
+instance Eq_Type1 (Type_Type0 (Proxy h0) root)
 
 -- | Convenient alias to include a 'Type_Bool' within a type.
-type_type0 :: Lift_Type_Root (Type_Type0 t0) root => root t0
-type_type0 = lift_type_root (Type_Type0 Proxy)
+type_type0 :: forall root h0. Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
+type_type0 = lift_type_root (Type_Type0 (Proxy::Proxy h0))
 
 -- ** Type 'Lift_Type'
 -- | Apply 'Peano_of_Type' on 'Lift_TypeP'.
@@ -390,47 +401,63 @@ unlift_type
 unlift_type = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 
 -- * Type 'Type_Type1'
-data Type_Type1 f (root:: * -> *) h where
-	Type_Type1 :: Proxy f -> root a -> Type_Type1 f root (f a)
-type instance Root_of_Type      (Type_Type1 f root) = root
-type instance Error_of_Type ast (Type_Type1 f root) = No_Error_Type
+data Type_Type1 px (root:: * -> *) h where
+	Type_Type1 :: px -> root a -> Type_Type1 px root ((Host1_of px) a)
+type instance Root_of_Type      (Type_Type1 px root) = root
+type instance Error_of_Type ast (Type_Type1 px root) = No_Error_Type
 
-instance Constraint_Type Eq  (Type_Type1 f root)
-instance Constraint_Type Ord (Type_Type1 f root)
+instance Constraint_Type Eq  (Type_Type1 (Proxy h1) root)
+instance Constraint_Type Ord (Type_Type1 (Proxy h1) root)
 
 instance -- Eq_Type
  Eq_Type root =>
- Eq_Type (Type_Type1 f root) where
-	eq_type (Type_Type1 _f1 a1) (Type_Type1 _f2 a2)
+ Eq_Type (Type_Type1 (Proxy h1) root) where
+	eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
 	 | Just Refl <- a1 `eq_type` a2
 	 = Just Refl
 	eq_type _ _ = Nothing
-instance -- Eq_Type1
- Eq_Type1 root =>
- Eq_Type1 (Type_Type1 f root) where
-	eq_type1 Type_Type1{} Type_Type1{}
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Type1 EPeano root) where
+	eq_type (Type_Type1 p1 a1)
+	        (Type_Type1 p2 a2)
+	 | p1 == p2
+	 , Just Refl <- a1 `eq_type` a2
 	 = Just Refl
+	eq_type _ _ = Nothing
+instance -- Eq
+ Eq_Type root =>
+ Eq (Type_Type1 (Proxy h1) root h) where
+	x == y = isJust $ eq_type x y
 instance -- Eq
  Eq_Type root =>
- Eq (Type_Type1 f root h) where
+ Eq (Type_Type1 EPeano root h) where
 	x == y = isJust $ eq_type x y
+instance -- Eq_Type1
+ Eq_Type1 (Type_Type1 (Proxy t1) root) where
+	eq_type1 Type_Type1{} Type_Type1{}
+	 = Just Refl
 instance -- Show
- String_from_Type (Type_Type1 f root) =>
- Show (Type_Type1 f root h) where
+ String_from_Type (Type_Type1 px root) =>
+ Show (Type_Type1 px root h) where
 	show = string_from_type
 
+-- ** Type 'Host1_of'
+type family Host1_of px :: * -> *
+type instance Host1_of (Proxy h1) = h1
+
 -- ** Type family 'May_be_Type1'
 type family May_be_Type1
  (ty:: (* -> *) -> * -> *) :: Bool where
-	May_be_Type1 (Type_Type1 f)                 = 'True
-	May_be_Type1 (Type_Alt (Type_Type1 f) next) = 'True
-	May_be_Type1 (Type_Alt curr next)           = May_be_Type1 next
-	May_be_Type1 ty                             = 'False
+	May_be_Type1 (Type_Type1 px)                 = 'True
+	May_be_Type1 (Type_Alt (Type_Type1 px) next) = 'True
+	May_be_Type1 (Type_Alt curr next)            = May_be_Type1 next
+	May_be_Type1 ty                              = 'False
 
 -- ** Type 'Lift_Type1'
-data Lift_Type1 f tys
+data Lift_Type1 px tys
  =   Lift_Type1 ( forall (root:: * -> *) h
-                . Type_Type1 f root h -> tys root h
+                . Type_Type1 px root h -> tys root h
                 )
 
 -- ** Type  'Unlift_Type1'
@@ -438,13 +465,13 @@ class Unlift_Type1 ty where
 	unlift_type1
 	 :: forall (root:: * -> *) ret h.
 	 ty root h
-	 -> (forall (f:: * -> *).
-	     ( Type_Type1 f root h
-	     , Lift_Type1 f ty
+	 -> (forall (px:: *).
+	     ( Type_Type1 px root h
+	     , Lift_Type1 px ty
 	     ) -> Maybe ret)
 	 -> Maybe ret
 	unlift_type1 _ty _k = Nothing
-instance Unlift_Type1 (Type_Type1 f) where
+instance Unlift_Type1 (Type_Type1 px) where
 	unlift_type1 ty k = k (ty, Lift_Type1 id)
 instance -- Type_Alt
  ( Unlift_Type1 curr
@@ -458,37 +485,61 @@ instance -- Type_Alt
 			Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
 
 -- * Type 'Type_Type2'
-data Type_Type2 c2 t2 (root:: * -> *) h where
-	Type_Type2 :: c2 a b => Proxy c2 -> Proxy t2 -> root a -> root b -> Type_Type2 c2 t2 root (t2 a b)
+data Type_Type2 px (root:: * -> *) h where
+	Type_Type2
+	 :: (Constraint2_of px) a b
+	 => px -> root a -> root b
+	 -> Type_Type2 px root ((Host2_of px) a b)
 class Constraint2_Empty a b
 instance Constraint2_Empty a b
 
-type instance Root_of_Type      (Type_Type2 c2 t2 root) = root
-type instance Error_of_Type ast (Type_Type2 c2 t2 root) = No_Error_Type
+type instance Root_of_Type      (Type_Type2 px root) = root
+type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
 
 instance -- Eq_Type
  Eq_Type root =>
- Eq_Type (Type_Type2 c2 t2 root) where
+ Eq_Type (Type_Type2 (Proxy h2) root) where
 	eq_type
-	 (Type_Type2 _ _ arg1 res1)
-	 (Type_Type2 _ _ arg2 res2)
+	 (Type_Type2 _ arg1 res1)
+	 (Type_Type2 _ arg2 res2)
 	 | Just Refl <- arg1 `eq_type` arg2
 	 , Just Refl <- res1 `eq_type` res2
 	 = Just Refl
 	eq_type _ _ = Nothing
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Type2 EPeano root) where
+	eq_type (Type_Type2 p1 arg1 res1)
+	        (Type_Type2 p2 arg2 res2)
+	 | p1 == p2
+	 , Just Refl <- arg1 `eq_type` arg2
+	 , Just Refl <- res1 `eq_type` res2
+	 = Just Refl
+	eq_type _ _ = Nothing
+instance -- Eq
+ Eq_Type root =>
+ Eq (Type_Type2 (Proxy h2) root h) where
+	x == y = isJust $ x `eq_type` y
 instance -- Eq
  Eq_Type root =>
- Eq (Type_Type2 c2 t2 root h) where
+ Eq (Type_Type2 EPeano root h) where
 	x == y = isJust $ x `eq_type` y
 instance -- Show
  ( String_from_Type root
- , String_from_Type (Type_Type2 c2 t2 root)
- ) => Show (Type_Type2 c2 t2 root h) where
+ , String_from_Type (Type_Type2 px root)
+ ) => Show (Type_Type2 px root h) where
 	show = string_from_type
-instance Constraint_Type Eq  (Type_Type2 c2 t2 root)
-instance Constraint_Type Ord (Type_Type2 c2 t2 root)
-instance Unlift_Type1 (Type_Type2 c2 t2)  -- FIXME: should be doable
-instance Eq_Type1 (Type_Type2 c2 t2 root) -- FIXME: should be doable
+instance Constraint_Type Eq  (Type_Type2 px root)
+instance Constraint_Type Ord (Type_Type2 px root)
+instance Unlift_Type1 (Type_Type2 px)  -- FIXME: should be doable
+instance Eq_Type1 (Type_Type2 px root) -- FIXME: should be doable
+
+-- ** Type 'Host2_of'
+type family Host2_of px :: * -> * -> *
+type instance Host2_of (Proxy h2) = h2
+
+-- ** Type 'Constraint2_of'
+type family Constraint2_of px :: (* -> * -> Constraint)
 
 -- * Type family 'Is_Last_Type'
 -- | Return whether a given type is the last one in a given type stack.
diff --git a/Language/Symantic/Type/Fun.hs b/Language/Symantic/Type/Fun.hs
index 0a1ecef..ef51f94 100644
--- a/Language/Symantic/Type/Fun.hs
+++ b/Language/Symantic/Type/Fun.hs
@@ -11,20 +11,37 @@
 module Language.Symantic.Type.Fun where
 
 import Data.Proxy
-
+import Data.Type.Equality ((:~:)(Refl))
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Fun'
 -- | The @->@ type.
 type Type_Fun lam
- = Type_Type2 Constraint2_Empty (Lambda lam)
+ = Type_Type2 (Proxy (Lambda lam))
+
+type instance Constraint2_of (Proxy (Lambda lam))
+ = Constraint2_Empty
+
+pattern Type_Fun
+ :: root arg -> root res
+ -> Type_Fun lam root ((Lambda lam) arg res)
 pattern Type_Fun arg res
- = Type_Type2 Proxy Proxy arg res
+ = Type_Type2 Proxy arg res
 
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Type2 (Proxy (Lambda lam)) root) where
+	eq_type
+	 (Type_Type2 _ arg1 res1)
+	 (Type_Type2 _ arg2 res2)
+	 | Just Refl <- arg1 `eq_type` arg2
+	 , Just Refl <- res1 `eq_type` res2
+	 = Just Refl
+	eq_type _ _ = Nothing
 instance -- String_from_Type
  String_from_Type root =>
  String_from_Type (Type_Fun lam root) where
-	string_from_type (Type_Type2 _ _ arg res) =
+	string_from_type (Type_Type2 _ arg res) =
 		"(" ++ string_from_type arg ++ " -> "
 		    ++ string_from_type res ++ ")"
 
diff --git a/Language/Symantic/Type/Int.hs b/Language/Symantic/Type/Int.hs
index 15548ad..6dd7e77 100644
--- a/Language/Symantic/Type/Int.hs
+++ b/Language/Symantic/Type/Int.hs
@@ -1,20 +1,25 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Int where
 
+import Data.Proxy
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Int'
 -- | The 'Int' type.
-type Type_Int = Type_Type0 Int
+type Type_Int = Type_Type0 (Proxy Int)
+
+pattern Type_Int :: Type_Type0 (Proxy Int) root Int
+pattern Type_Int  = Type_Type0 Proxy
 
 instance -- String_from_Type
  String_from_Type (Type_Int root) where
 	string_from_type _ = "Int"
 
--- | Convenient alias to include a 'Type_Int' within a type.
+-- | Inject 'Type_Int' within a root type.
 type_int :: Lift_Type_Root Type_Int root => root Int
 type_int = type_type0
diff --git a/Language/Symantic/Type/List.hs b/Language/Symantic/Type/List.hs
index 555082c..f263a5c 100644
--- a/Language/Symantic/Type/List.hs
+++ b/Language/Symantic/Type/List.hs
@@ -1,24 +1,39 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.List where
 
 import Data.Proxy
-
+import Data.Type.Equality ((:~:)(Refl))
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_List'
 -- | The list type.
-type Type_List = Type_Type1 []
+type Type_List = Type_Type1 (Proxy [])
+
+pattern Type_List :: root a -> Type_List root ([] a)
+pattern Type_List a = Type_Type1 Proxy a
 
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Type1 (Proxy []) root) where
+	eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
+	 | Just Refl <- a1 `eq_type` a2
+	 = Just Refl
+	eq_type _ _ = Nothing
+instance -- Eq_Type1
+ Eq_Type1 (Type_Type1 (Proxy []) root) where
+	eq_type1 Type_Type1{} Type_Type1{}
+	 = Just Refl
 instance -- String_from_Type
  String_from_Type root =>
  String_from_Type (Type_List root) where
 	string_from_type (Type_Type1 _f a) =
 		"[" ++ string_from_type a ++ "]"
 
--- | Inject a 'Type_List' within a root type.
+-- | Inject 'Type_List' within a root type.
 type_list
  :: Lift_Type_Root Type_List root
  => root h_a
diff --git a/Language/Symantic/Type/Map.hs b/Language/Symantic/Type/Map.hs
index debee62..4b32750 100644
--- a/Language/Symantic/Type/Map.hs
+++ b/Language/Symantic/Type/Map.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Map where
 
 import Data.Proxy
@@ -15,10 +16,18 @@ import Language.Symantic.Type.Common
 
 -- * Type 'Type_Map'
 -- | The 'Map' type.
-type Type_Map
- = Type_Type2 Constraint2_Map Map
-pattern Type_Map arg res
- = Type_Type2 Proxy Proxy arg res
+type Type_Map = Type_Type2 (Proxy Map)
+
+type instance Constraint2_of (Proxy Map)
+ = Constraint2_Map
+
+{- FIXME: Could not deduce (Ord k) arising from a pattern…
+pattern Type_Map
+ :: Ord k => root k -> root a
+ -> Type_Type2 (Proxy Map) root (Map k a)
+pattern Type_Map k a
+ = Type_Type2 Proxy k a
+-}
 
 -- ** Class 'Constraint2_Map'
 class Constraint2_Map k a
@@ -27,15 +36,15 @@ instance Ord k => Constraint2_Map k a
 instance -- String_from_Type
  String_from_Type root =>
  String_from_Type (Type_Map root) where
-	string_from_type (Type_Type2 _ _ k a) =
+	string_from_type (Type_Type2 _ k a) =
 		"Map (" ++ string_from_type k ++ ")"
 		 ++ " (" ++ string_from_type a ++ ")"
 
--- | Convenient alias to include a 'Type_Map' within a type.
+-- | Inject 'Type_Map' within a root type.
 type_map
  :: forall root h_k h_a.
  (Lift_Type_Root Type_Map root, Ord h_k)
  => root h_k -> root h_a
  -> root (Map h_k h_a)
-type_map k a = lift_type_root (Type_Map k a
+type_map k a = lift_type_root (Type_Type2 Proxy k a
 	 ::Type_Map root (Map h_k h_a))
diff --git a/Language/Symantic/Type/Maybe.hs b/Language/Symantic/Type/Maybe.hs
index 83fb1f3..05d6271 100644
--- a/Language/Symantic/Type/Maybe.hs
+++ b/Language/Symantic/Type/Maybe.hs
@@ -1,24 +1,39 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Maybe where
 
 import Data.Proxy
-
+import Data.Type.Equality ((:~:)(Refl))
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Maybe'
 -- | The 'Maybe' type.
-type Type_Maybe = Type_Type1 Maybe
+type Type_Maybe = Type_Type1 (Proxy Maybe)
+
+pattern Type_Map :: root a -> Type_Maybe root (Maybe a)
+pattern Type_Map a = Type_Type1 Proxy a
 
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Type1 (Proxy Maybe) root) where
+	eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
+	 | Just Refl <- a1 `eq_type` a2
+	 = Just Refl
+	eq_type _ _ = Nothing
+instance -- Eq_Type1
+ Eq_Type1 (Type_Type1 (Proxy Maybe) root) where
+	eq_type1 Type_Type1{} Type_Type1{}
+	 = Just Refl
 instance -- String_from_Type
  String_from_Type root =>
  String_from_Type (Type_Maybe root) where
 	string_from_type (Type_Type1 _f a) =
 		"Maybe" ++ " (" ++ string_from_type a ++ ")"
 
--- | Inject a 'Type_Maybe' within a root type.
+-- | Inject 'Type_Maybe' within a root type.
 type_maybe
  :: Lift_Type_Root Type_Maybe root
  => root h_a
diff --git a/Language/Symantic/Type/Ordering.hs b/Language/Symantic/Type/Ordering.hs
index 7c93c63..c3d9e28 100644
--- a/Language/Symantic/Type/Ordering.hs
+++ b/Language/Symantic/Type/Ordering.hs
@@ -1,19 +1,24 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Ordering where
 
+import Data.Proxy
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Ordering'
 -- | The 'Ordering' type.
-type Type_Ordering = Type_Type0 Ordering
+type Type_Ordering = Type_Type0 (Proxy Ordering)
+
+pattern Type_Ordering :: Type_Ordering root Ordering
+pattern Type_Ordering  = Type_Type0 Proxy
 
 instance -- String_from_Type
  String_from_Type (Type_Ordering root) where
 	string_from_type _ = "Ordering"
 
--- | Convenient alias to include a 'Type_Ordering' within a type.
+-- | Inject 'Type_Ordering' within a root type.
 type_ordering :: Lift_Type_Root Type_Ordering root => root Ordering
 type_ordering = type_type0
diff --git a/Language/Symantic/Type/Tuple.hs b/Language/Symantic/Type/Tuple.hs
index 9e1ad2b..72651d3 100644
--- a/Language/Symantic/Type/Tuple.hs
+++ b/Language/Symantic/Type/Tuple.hs
@@ -7,29 +7,35 @@
 module Language.Symantic.Type.Tuple where
 
 import Data.Proxy
-
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Tuple2'
 -- | The (,) type.
-type Type_Tuple2
- = Type_Type2 Constraint2_Empty (,)
-pattern Type_Tuple2 arg res
- = Type_Type2 Proxy Proxy arg res
+type Type_Tuple2 = Type_Type2 (Proxy (,))
+
+type instance Constraint2_of (Proxy (,))
+ = Constraint2_Empty
+
+pattern Type_Tuple2
+ :: root a -> root b
+ -> Type_Tuple2 root ((,) a b)
+pattern Type_Tuple2 a b
+ = Type_Type2 Proxy a b
 
 instance -- String_from_Type
  String_from_Type root =>
  String_from_Type (Type_Tuple2 root) where
-	string_from_type (Type_Type2 _ _ a b) =
+	string_from_type (Type_Type2 _ a b) =
 		"("  ++ string_from_type a ++
 		", " ++ string_from_type b ++ ")"
 
--- | Convenient alias to include a 'Type_Tuple2' within a type.
+-- | Inject 'Type_Tuple2' within a root type.
 type_tuple2
  :: forall root h_a h_b.
  Lift_Type_Root Type_Tuple2 root
  => root h_a
  -> root h_b
  -> root (h_a, h_b)
-type_tuple2 a b = lift_type_root (Type_Tuple2 a b
+type_tuple2 a b = lift_type_root
+	 (Type_Tuple2 a b
 	 ::Type_Tuple2 root (h_a, h_b))
diff --git a/Language/Symantic/Type/Unit.hs b/Language/Symantic/Type/Unit.hs
index 0e076ec..28d1eef 100644
--- a/Language/Symantic/Type/Unit.hs
+++ b/Language/Symantic/Type/Unit.hs
@@ -1,20 +1,25 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Type.Unit where
 
+import Data.Proxy
 import Language.Symantic.Type.Common
 
 -- * Type 'Type_Unit'
 -- | The @()@ type.
-type Type_Unit = Type_Type0 ()
+type Type_Unit = Type_Type0 (Proxy ())
+
+pattern Type_Unit :: Type_Unit root ()
+pattern Type_Unit  = Type_Type0 Proxy
 
 instance -- String_from_Type
  String_from_Type (Type_Unit root) where
 	string_from_type _ = "()"
 
--- | Convenient alias to include a 'Type_Unit' within a type.
+-- | Inject 'Type_Unit' within a root type.
 type_unit :: Lift_Type_Root Type_Unit root => root ()
 type_unit = type_type0
diff --git a/Language/Symantic/Type/Var.hs b/Language/Symantic/Type/Var.hs
index 7f06ed9..85914ed 100644
--- a/Language/Symantic/Type/Var.hs
+++ b/Language/Symantic/Type/Var.hs
@@ -1,36 +1,86 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 -- | Type variable.
 module Language.Symantic.Type.Var
  ( module Language.Symantic.Type.Var
  , module Language.Symantic.Lib.Data.Peano
  ) where
 
-import Data.Maybe (isJust)
-
+import Data.Type.Equality ((:~:)(Refl))
 import Language.Symantic.Type.Common
 import Language.Symantic.Lib.Data.Peano
 
--- * Type 'Type_Var'
+-- * Type 'Var0'
+newtype Var0 = Var0 EPeano
+type instance Host_of EPeano = Var0
+
+-- | Undefined instance required to build errors.
+instance Eq Var0
+-- | Undefined instance required to build errors.
+instance Ord Var0
+
+-- * Type 'Var1'
+newtype Var1 a = Var1 EPeano
+type instance Host1_of EPeano = Var1
+
+-- * Type 'Type_Var0'
+-- | The variable type.
+type Type_Var0 = Type_Type0 EPeano
+
+pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
+pattern Type_Var0 p = Type_Type0 (EPeano p)
+
+instance Eq_Type1 (Type_Var0 root) where
+instance -- String_from_Type
+ String_from_Type (Type_Var0 root) where
+	string_from_type (Type_Type0 (EPeano p)) =
+		"t" ++ show (integral_from_peano p::Integer)
+instance Constraint_Type Eq (Type_Var0 root) where
+	constraint_type _c Type_Type0{} = Just Dict
+
+-- | Inject 'Type_Var0' within a root type.
+type_var0 :: Lift_Type_Root Type_Var0 root => SPeano p -> root Var0
+type_var0 = lift_type_root . Type_Type0 . EPeano
+
+-- * Type 'Type_Var1'
 -- | The variable type.
-data Type_Var (root:: * -> *) p where
-	Type_Var :: SPeano p -> Type_Var root p
-type instance Root_of_Type      (Type_Var root) = root
-type instance Error_of_Type ast (Type_Var root) = No_Error_Type
+type Type_Var1 = Type_Type1 EPeano
+instance Constraint_Type Eq (Type_Var1 root)
+
+pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
+pattern Type_Var1 p a = Type_Type1 (EPeano p) a
+
+instance Eq_Type1 (Type_Var1 root) where
+	eq_type1 (Type_Type1 p1 _) (Type_Type1 p2 _)
+	 | p1 == p2
+	 = Just Refl
+	eq_type1 _ _ = Nothing
+instance -- String_from_Type
+ String_from_Type root =>
+ String_from_Type (Type_Var1 root) where
+	string_from_type (Type_Type1 (EPeano p) a) =
+		"t_" ++ show (integral_from_peano p::Integer) ++
+		" " ++ string_from_type a
 
+-- | Inject 'Type_Var1' within a root type.
+type_var1 :: Lift_Type_Root Type_Var1 root => SPeano p -> root a -> root (Var1 a)
+type_var1 p = lift_type_root . Type_Var1 p
+
+{-
 instance -- Eq_Type
  Eq_Type (Type_Var root) where
 	eq_type (Type_Var x) (Type_Var y) = x `peano_eq` y
 instance -- Eq
  Eq (Type_Var root h) where
 	x == y = isJust $ x `eq_type` y
-instance -- String_from_Type
- String_from_Type (Type_Var root) where
-	string_from_type (Type_Var p) =
-		"t" ++ show (integral_from_peano p::Integer)
 instance -- Show
  Show (Type_Var root h) where
 	show = string_from_type
@@ -38,7 +88,4 @@ instance Constraint_Type Eq  (Type_Var root)
 instance Constraint_Type Ord (Type_Var root)
 instance Unlift_Type1 Type_Var
 instance Eq_Type1 (Type_Var root)
-
--- | Convenient alias to include a 'Type_Var' within a type.
-type_var :: Lift_Type_Root Type_Var root => SPeano p -> root p
-type_var = lift_type_root . Type_Var
+-}
-- 
2.47.2