diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal
index 34502297..628ee7b2 100644
--- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal
+++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal
@@ -48,6 +48,7 @@ common common-language
     FlexibleInstances
     ForeignFunctionInterface
     GADTSyntax
+    GeneralizedNewtypeDeriving
     HexFloatLiterals
     ImportQualifiedPost
     InstanceSigs
@@ -64,6 +65,7 @@ common common-language
     PolyKinds
     PostfixOperators
     RankNTypes
+    RecordWildCards
     RelaxedPolyRec
     ScopedTypeVariables
     StandaloneDeriving
@@ -79,15 +81,19 @@ common common-language
 
   default-language:   Haskell2010
 
+common common-imports
+  build-depends:
+    , base  >=4.16
+    , lens  >=5.2
+
 library
   import:          common-language
+  import:          common-imports
   build-depends:
-    , base                        >=4.16
-    , containers                  >=0.6
+    , containers                  >=0.6.5.1
     , freer-simple                >=1.2
     , generic-lens                >=2.2
     , lambda-buffers-compiler-pb  >=0.1.0.0
-    , lens                        >=5.2
     , mtl                         >=2.2
     , parsec                      >=3.1
     , prettyprinter               >=1.7
@@ -96,7 +102,11 @@ library
 
   exposed-modules:
     LambdaBuffers.Compiler.KindCheck
+    LambdaBuffers.Compiler.KindCheck.Context
     LambdaBuffers.Compiler.KindCheck.Inference
+    LambdaBuffers.Compiler.KindCheck.Kind
+    LambdaBuffers.Compiler.KindCheck.Type
+    LambdaBuffers.Compiler.KindCheck.Variable
     LambdaBuffers.Compiler.NamingCheck
     LambdaBuffers.Compiler.ProtoCompat
     LambdaBuffers.Compiler.ProtoCompat.Types
@@ -106,13 +116,12 @@ library
 
 executable lambda-buffers-compiler-cli
   import:         common-language
+  import:         common-imports
   main-is:        Main.hs
   build-depends:
-    , base                        >=4.16
     , bytestring                  >=0.11
     , lambda-buffers-compiler
     , lambda-buffers-compiler-pb  >=0.1.0.0
-    , lens                        >=5.2
     , optparse-applicative        >=0.17
     , proto-lens                  >=0.7
     , text                        >=1.2
@@ -122,14 +131,13 @@ executable lambda-buffers-compiler-cli
 
 test-suite tests
   import:         common-language
+  import:         common-imports
   type:           exitcode-stdio-1.0
   hs-source-dirs: test
   main-is:        Test.hs
   build-depends:
-    , base                        >=4.16
     , lambda-buffers-compiler
     , lambda-buffers-compiler-pb  >=0.1
-    , lens                        >=5.2
     , proto-lens                  >=0.7
     , tasty                       >=1.4
     , tasty-hunit                 >=0.10
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs
index ef81abf3..1ad4b088 100644
--- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs
@@ -1,240 +1,355 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
 
-{- | FIXME(cstml): At the moment the Kind Checker disregards multiple Modules for
-simplicity of testing and developing. This will be changed ASAP.
--}
 module LambdaBuffers.Compiler.KindCheck (
   KindCheckFailure (..),
-  runKindCheck,
-  TypeDefinition (..),
+  check,
+  foldWithSum,
 
   -- * Testing Utils
-  kindCheckType,
-  runKindCheckEff,
+
+  -- * Utilities -- exported for testing
+  foldWithArrow,
+  foldWithProduct,
 ) where
 
 import Control.Exception (Exception)
-import Control.Lens (folded, makeLenses, to, (&), (.~), (^.), (^..))
-import Control.Monad.Freer (Eff, interpret, run)
+import Control.Lens (view, (&), (.~), (^.))
+import Control.Monad (void)
+import Control.Monad.Freer (Eff, Members, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
+import Control.Monad.Freer.Reader (Reader, ask, runReader)
 import Control.Monad.Freer.TH (makeEffect)
-import Data.Text (Text, intercalate, unpack)
+import Data.Text (Text, intercalate)
+import LambdaBuffers.Compiler.KindCheck.Context (Context, getAllContext)
 import LambdaBuffers.Compiler.KindCheck.Inference (
-  Context,
   InferErr,
   Kind (Type, (:->:)),
-  Type (Abs, App, Var),
+  Type (Abs, Var),
   context,
   infer,
  )
+import LambdaBuffers.Compiler.KindCheck.Type (Type (App))
+import LambdaBuffers.Compiler.KindCheck.Variable (Var)
+import LambdaBuffers.Compiler.ProtoCompat qualified as P
 
-import Control.Monad (void)
-import Data.Traversable (for)
-import Proto.Compiler (
-  Product'NTuple,
-  Product'Product (Product'Ntuple, Product'Record'),
-  Product'Record,
-  Sum,
-  Ty,
-  Ty'Ty (Ty'TyApp, Ty'TyRef, Ty'TyVar),
-  TyApp,
-  TyBody'TyBody (TyBody'Opaque, TyBody'Sum),
-  TyDef,
-  TyRef,
-  TyRef'TyRef (TyRef'ForeignTyRef, TyRef'LocalTyRef),
- )
-import Proto.Compiler_Fields as PF (
-  argName,
-  constrName,
-  constructors,
-  fieldTy,
-  fields,
-  maybe'product,
-  maybe'ty,
-  maybe'tyBody,
-  maybe'tyRef,
-  moduleName,
-  name,
-  parts,
-  product,
-  tyAbs,
-  tyArgs,
-  tyBody,
-  tyFunc,
-  tyName,
-  varName,
- )
+import Data.Foldable (traverse_)
+import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|))
+import Data.Map qualified as M
 
 --------------------------------------------------------------------------------
 -- Types
 
+-- FIXME(cstml) - We should add the following tests:
+-- - double declaration of a type
+
 -- | Kind Check failure types.
 data KindCheckFailure
   = CheckFailure String
   | LookupVarFailure Text
-  | LookupRefFailure TyRef
+  | LookupRefFailure P.TyRef
   | AppWrongArgKind Kind Kind -- Expected Kind got Kind
   | AppToManyArgs Int
   | InvalidProto Text
   | AppNoArgs -- No args
-  | InvalidType
-  | InferenceFailed TypeDefinition InferErr
+  | InvalidType InferErr
+  | InferenceFailed P.TyDef InferErr
+  | InconsistentType P.TyDef
   deriving stock (Show, Eq)
 
 instance Exception KindCheckFailure
 
-{- | Validated Type Definition.
- :fixme: Add to compiler.proto
--}
-data TypeDefinition = TypeDefinition
-  { _td'name :: String
-  , _td'variables :: [String]
-  , _td'sop :: Type
-  }
-  deriving stock (Show, Eq)
+type Err = Error KindCheckFailure
 
-makeLenses 'TypeDefinition
+type ModName = Text
 
-data KindCheck a where
-  ValidateInput :: [TyDef] -> KindCheck [TypeDefinition]
-  CreateContext :: [TypeDefinition] -> KindCheck Context
-  KindCheck :: Context -> TypeDefinition -> KindCheck Kind
+-- | Main interface to the Kind Checker.
+data Check a where
+  KCheck :: P.CompilerInput -> Check ()
 
-makeEffect ''KindCheck
+makeEffect ''Check
+
+-- | Interactions that happen at the level of the Global Checker.
+data GlobalCheck a where
+  CreateContext :: P.CompilerInput -> GlobalCheck Context
+  ValidateModule :: Context -> P.Module -> GlobalCheck ()
+
+makeEffect ''GlobalCheck
 
-type KindCheckFailEff = '[Error KindCheckFailure]
-type KindCheckEff = KindCheck ': KindCheckFailEff
+-- | Interactions that happen at the level of the
+data ModuleCheck a where -- Module
+  KCTypeDefinition :: ModName -> Context -> P.TyDef -> ModuleCheck Kind
+  KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck ()
+  KCClass :: Context -> P.ClassDef -> ModuleCheck ()
+
+makeEffect ''ModuleCheck
+
+data KindCheck a where
+  KindFromTyDef :: ModName -> P.TyDef -> KindCheck Type
+  InferTypeKind :: Context -> Type -> KindCheck Kind
+  CheckKindConsistency :: ModName -> P.TyDef -> Context -> Kind -> KindCheck Kind
+makeEffect ''KindCheck
 
 --------------------------------------------------------------------------------
--- API
 
--- | Main Kind Checking function
-runKindCheck :: [TyDef] -> Either KindCheckFailure ()
-runKindCheck tDefs = void $ run $ runError $ interpretKindCheck $ kindCheckDefs tDefs
+runCheck :: Eff (Check ': '[]) a -> Either KindCheckFailure a
+runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
 
-runKindCheckEff :: Eff KindCheckEff a -> Either KindCheckFailure a
-runKindCheckEff = run . runError . interpretKindCheck
+check :: P.CompilerInput -> Either KindCheckFailure ()
+check = runCheck . kCheck
 
 --------------------------------------------------------------------------------
--- Strategy
-
--- | Strategy for kind checking.
-kindCheckDefs :: [TyDef] -> Eff KindCheckEff ()
-kindCheckDefs tyDefs = validateInput tyDefs >>= void . kindCheckType
-
-kindCheckType :: [TypeDefinition] -> Eff KindCheckEff [Kind]
-kindCheckType validTDef = do
-  ctx <- createContext validTDef
-  traverse (kindCheck ctx) validTDef
-
-interpretKindCheck :: Eff KindCheckEff a -> Eff '[Error KindCheckFailure] a
-interpretKindCheck = interpret $
-  \case
-    ValidateInput tDs -> validateTyDef `traverse` tDs
-    CreateContext tDs -> mconcat <$> makeContext `traverse` tDs
-    KindCheck ctx tD -> either (convertError tD) pure $ infer ctx (tD ^. td'sop)
+
+type Transform x y = forall effs {a}. Eff (x ': effs) a -> Eff (y ': effs) a
+
+-- Transformation strategies
+globalStrategy :: Transform Check GlobalCheck
+globalStrategy = reinterpret $ \case
+  KCheck ci -> do
+    ctx <- createContext ci
+    void $ validateModule ctx `traverse` (ci ^. #modules)
+
+moduleStrategy :: Transform GlobalCheck ModuleCheck
+moduleStrategy = reinterpret $ \case
+  CreateContext ci -> resolveCreateContext ci
+  ValidateModule cx md -> do
+    traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs)
+    traverse_ (kCClassInstance cx) (md ^. #instances)
+    traverse_ (kCClass cx) (md ^. #classDefs)
+
+localStrategy :: Transform ModuleCheck KindCheck
+localStrategy = reinterpret $ \case
+  KCTypeDefinition mname ctx tydef -> do
+    kindFromTyDef mname tydef >>= inferTypeKind ctx >>= checkKindConsistency mname tydef ctx
+  KCClassInstance _ctx _instClause -> pure () -- "FIXME(cstml)"
+  KCClass _ctx _classDef -> pure () --  "FIXME(cstml)"
+
+runKindCheck :: Eff '[KindCheck] a -> Eff '[Err] a
+runKindCheck = reinterpret $ \case
+  KindFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef)
+  InferTypeKind ctx ty -> either (throwError . InvalidType) pure $ infer ctx ty
+  CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k
+
+-- Resolvers
+
+resolveKindConsistency ::
+  forall effs.
+  Members '[Reader ModName, Err] effs =>
+  P.TyDef ->
+  Context ->
+  Kind ->
+  Eff effs Kind
+resolveKindConsistency tydef ctx inferredKind = do
+  mName <- ask @ModName
+  (n, k) <- tyDef2NameAndKind mName tydef
+  guard $ k == inferredKind
+  guard $ getAllContext ctx M.!? n == Just inferredKind
+  pure inferredKind
   where
-    convertError :: forall a. TypeDefinition -> InferErr -> Eff KindCheckFailEff a
-    convertError td = throwError . InferenceFailed td
+    guard b = if b then pure () else throwError $ InconsistentType tydef
+
+resolveCreateContext :: forall effs. P.CompilerInput -> Eff effs Context
+resolveCreateContext ci = mconcat <$> traverse module2Context (ci ^. #modules)
+
+module2Context :: forall effs. P.Module -> Eff effs Context
+module2Context m = mconcat <$> traverse (tyDef2Context (flattenModuleName (m ^. #moduleName))) (P.typeDefs m)
+
+flattenModuleName :: P.ModuleName -> Text
+flattenModuleName mName = intercalate "." $ (\p -> p ^. #name) <$> mName ^. #parts
+
+tyDef2NameAndKind :: forall effs. ModName -> P.TyDef -> Eff effs (ModName, Kind)
+tyDef2NameAndKind curModName tyDef = do
+  let name = curModName <> "." <> (tyDef ^. #tyName . #name) -- name is qualified
+  let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
+  pure (name, k)
+
+tyDef2Context :: forall effs. ModName -> P.TyDef -> Eff effs Context
+tyDef2Context curModName tyDef = do
+  r <- tyDef2NameAndKind curModName tyDef
+  pure $ mempty & context .~ uncurry M.singleton r
+
+tyAbsLHS2Kind :: P.TyAbs -> Kind
+tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs)
+
+foldWithArrow :: [Kind] -> Kind
+foldWithArrow = foldl (:->:) Type
+
+-- ================================================================================
+-- To Kind Conversion functions
+
+pKind2Type :: P.Kind -> Kind
+pKind2Type k =
+  case k ^. #kind of
+    P.KindRef P.KType -> Type
+    P.KindArrow l r -> pKind2Type l :->: pKind2Type r
+    -- FIXME(cstml) what is an undefined type meant to mean?
+    _ -> error "Fixme undefined type"
+
+-- =============================================================================
+-- X To Canonical type conversion functions.
+
+-- | TyDef to Kind Canonical representation.
+tyDef2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.TyDef ->
+  Eff eff Type
+tyDef2Type tyde = tyAbsLHS2Type (tyde ^. #tyAbs) <*> tyAbsRHS2Type (tyde ^. #tyAbs)
+
+tyAbsLHS2Type ::
+  forall eff.
+  P.TyAbs ->
+  Eff eff (Type -> Type)
+tyAbsLHS2Type tyab = tyArgs2Type (tyab ^. #tyArgs)
+
+tyArgs2Type ::
+  forall eff.
+  [P.TyArg] ->
+  Eff eff (Type -> Type)
+tyArgs2Type = \case
+  [] -> pure id
+  x : xs -> do
+    f <- tyArgs2Type xs
+    pure $ \c -> Abs (tyArg2Var x) (f c)
+
+tyArg2Var :: P.TyArg -> Var
+tyArg2Var = view (#argName . #name)
+
+tyAbsRHS2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.TyAbs ->
+  Eff eff Type
+tyAbsRHS2Type tyab = tyBody2Type (tyab ^. #tyBody)
+
+tyBody2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.TyBody ->
+  Eff eff Type
+tyBody2Type = \case
+  P.OpaqueI _ -> pure $ Var "Opaque"
+  P.SumI s -> sum2Type s
+
+sum2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Sum ->
+  Eff eff Type
+sum2Type su = foldWithSum <$> traverse constructor2Type (su ^. #constructors)
+
+constructor2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Constructor ->
+  Eff eff Type
+constructor2Type co = product2Type (co ^. #product)
+
+product2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Product ->
+  Eff eff Type
+product2Type = \case
+  P.RecordI r -> record2Type r
+  P.TupleI t -> tuple2Type t
+
+record2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Record ->
+  Eff eff Type
+record2Type r = foldWithProduct <$> traverse field2Type (r ^. #fields)
+
+tuple2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Tuple ->
+  Eff eff Type
+tuple2Type tu = do
+  tup <- traverse ty2Type $ tu ^. #fields
+  case tup of
+    [] -> pure $ Var "𝟙"
+    x : xs -> pure . foldWithProduct $ x :| xs
+
+field2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Field ->
+  Eff eff Type
+field2Type f = ty2Type (f ^. #fieldTy)
+
+ty2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.Ty ->
+  Eff eff Type
+ty2Type = \case
+  P.TyVarI tytv -> tyVar2Type tytv
+  P.TyAppI tyap -> tyApp2Type tyap
+  P.TyRefI tyre -> tyRef2Type tyre
+
+tyVar2Type ::
+  forall eff.
+  P.TyVar ->
+  Eff eff Type
+tyVar2Type tv = pure . Var $ (tv ^. #varName . #name)
+
+tyApp2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.TyApp ->
+  Eff eff Type
+tyApp2Type ta = do
+  fn <- ty2Type (ta ^. #tyFunc)
+  args <- traverse ty2Type (ta ^. #tyArgs)
+  pure $ foldWithApp (fn <| args)
+
+tyRef2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.TyRef ->
+  Eff eff Type
+tyRef2Type = \case
+  P.LocalI lref -> localTyRef2Type lref
+  P.ForeignI fref -> foreignTyRef2Type fref
+
+localTyRef2Type ::
+  forall eff.
+  Members '[Reader ModName, Err] eff =>
+  P.LocalRef ->
+  Eff eff Type
+localTyRef2Type ltr = do
+  moduleName <- ask
+  pure $ Var $ moduleName <> "." <> (ltr ^. #tyName . #name)
+
+foreignTyRef2Type ::
+  forall eff.
+  P.ForeignRef ->
+  Eff eff Type
+foreignTyRef2Type ftr = do
+  let moduleName = flattenModuleName (ftr ^. #moduleName)
+  pure $ Var $ moduleName <> "." <> (ftr ^. #tyName . #name)
 
 --------------------------------------------------------------------------------
--- Implementation
-
-validateTyDef :: TyDef -> Eff KindCheckFailEff TypeDefinition
-validateTyDef tD = do
-  let vars = tD ^.. tyAbs . tyArgs . folded . argName . name . to unpack
-  sop <- go (tD ^. tyAbs . tyBody . maybe'tyBody)
-  pure $
-    TypeDefinition
-      { _td'name = tD ^. tyName . name . to unpack
-      , _td'variables = vars
-      , _td'sop = foldVars vars sop
-      }
-  where
-    go = \case
-      Just body -> tyBodyToType body
-      Nothing -> throwError $ InvalidProto "Type Definition must have a body"
-
-    foldVars vs ts = case vs of
-      [] -> ts
-      x : xs -> Abs x (foldVars xs ts)
-
-tyBodyToType :: TyBody'TyBody -> Eff KindCheckFailEff Type
-tyBodyToType = \case
-  TyBody'Opaque _ -> pure $ Var "Opaque"
-  TyBody'Sum sumB -> sumToType sumB
-
-sumToType :: Sum -> Eff KindCheckFailEff Type
-sumToType sumT = do
-  let _constrNames :: [String] = sumT ^.. constructors . folded . constrName . name . to unpack
-      products :: [Maybe Product'Product] = sumT ^.. constructors . folded . PF.product . maybe'product
-  sumTRes <-
-    for
-      products
-      $ \case
-        Just (Product'Ntuple nt) -> nTupleToType nt
-        Just (Product'Record' re) -> recordToType re
-        Nothing -> throwError $ InvalidProto "Every constructor should have a product defining it"
-  foldWithEither sumTRes
-
-nTupleToType :: Product'NTuple -> Eff KindCheckFailEff Type
-nTupleToType nt = do
-  let fs :: [Ty] = nt ^. fields
-  prodT <- tyToType `traverse` fs
-  foldWithTuple prodT
-
-recordToType :: Product'Record -> Eff KindCheckFailEff Type
-recordToType rcrd = do
-  let x :: [Ty] = rcrd ^.. fields . folded . fieldTy
-  tC <- tyToType `traverse` x
-  foldWithTuple tC
-
--- old version: foldr ($) (Var "()") . fmap (App . App (Var "(,)"))
-foldWithTuple :: [Type] -> Eff KindCheckFailEff Type
-foldWithTuple = foldWithBinaryOp $ App . App (Var "(,)")
-
--- old version foldr ($) (Var "Void") . fmap (App . App (Var "Either"))
-foldWithEither :: [Type] -> Eff KindCheckFailEff Type
-foldWithEither = foldWithBinaryOp $ App . App (Var "Either")
+-- Utilities
+
+foldWithApp :: NonEmpty Type -> Type
+foldWithApp = foldWithBinaryOp App
+
+foldWithProduct :: NonEmpty Type -> Type
+foldWithProduct = foldWithBinaryOp $ App . App (Var "Π")
+
+foldWithSum :: NonEmpty Type -> Type
+foldWithSum = foldWithBinaryOp $ App . App (Var "Σ")
 
 -- | Generic way of folding.
-foldWithBinaryOp :: (Type -> Type -> Type) -> [Type] -> Eff KindCheckFailEff Type
-foldWithBinaryOp op = \case
-  [] -> throwError InvalidType
-  [x] -> pure x
-  x : xs -> op x <$> foldWithTuple xs
-
-tyToType :: Ty -> Eff KindCheckFailEff Type
-tyToType ty = do
-  case ty ^. maybe'ty of
-    Just (Ty'TyVar v) -> pure $ Var (v ^. varName . name . to unpack)
-    Just (Ty'TyApp app) -> tyAppToType app
-    Just (Ty'TyRef ref) -> tyRefToType ref
-    Nothing -> throwError $ InvalidProto "Type is not defined"
-
-tyAppToType :: TyApp -> Eff KindCheckFailEff Type
-tyAppToType tApp = do
-  fC <- tyToType (tApp ^. tyFunc)
-  fArgsC <- tyToType `traverse` (tApp ^. tyArgs)
-  case fArgsC of
-    [] -> throwError AppNoArgs
-    _ -> pure $ appF fC fArgsC
-  where
-    appF t [] = t
-    appF t (x : xs) = appF (App t x) xs
+foldWithBinaryOp :: (Type -> Type -> Type) -> NonEmpty Type -> Type
+foldWithBinaryOp op ne = case uncons ne of
+  (x, Nothing) -> x
+  (x, Just xs) -> op x $ foldWithBinaryOp op xs
 
-makeContext :: TypeDefinition -> Eff KindCheckFailEff Context
-makeContext td =
-  pure $ mempty & context .~ [(td ^. td'name, g (td ^. td'variables))]
-  where
-    g :: [a] -> Kind
-    g = \case
-      [] -> Type
-      (_ : xs) -> Type :->: g xs
-
-tyRefToType :: TyRef -> Eff KindCheckFailEff Type
-tyRefToType tR = do
-  case tR ^. maybe'tyRef of
-    Just (TyRef'LocalTyRef t) -> pure $ Var $ t ^. tyName . name . to unpack
-    Just (TyRef'ForeignTyRef t) -> pure $ Var $ (t ^. moduleName . parts . to (\ps -> unpack $ intercalate "." [p ^. name | p <- ps])) <> "." <> (t ^. tyName . name . to unpack)
-    Nothing -> throwError $ InvalidProto "TyRef Cannot be empty"
+module2ModuleName :: P.Module -> ModName
+module2ModuleName = flattenModuleName . (^. #moduleName)
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Context.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Context.hs
new file mode 100644
index 00000000..442e3b26
--- /dev/null
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Context.hs
@@ -0,0 +1,41 @@
+module LambdaBuffers.Compiler.KindCheck.Context (Context (Context), context, addContext, getAllContext) where
+
+import Control.Lens (makeLenses, (^.))
+import Data.Map qualified as M
+import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
+import LambdaBuffers.Compiler.KindCheck.Variable (Atom)
+import Prettyprinter (
+  Doc,
+  Pretty (pretty),
+  braces,
+  comma,
+  hsep,
+  punctuate,
+  (<+>),
+ )
+
+data Context = Context
+  { _context :: M.Map Atom Kind
+  , _addContext :: M.Map Atom Kind
+  }
+  deriving stock (Show, Eq)
+
+makeLenses ''Context
+
+instance Pretty Context where
+  pretty c = case M.toList (c ^. addContext) of
+    [] -> "Γ"
+    ctx -> "Γ" <+> "∪" <+> braces (setPretty ctx)
+    where
+      setPretty :: [(Atom, Kind)] -> Doc ann
+      setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
+
+instance Semigroup Context where
+  (Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2)
+
+instance Monoid Context where
+  mempty = Context mempty mempty
+
+-- | Utility to unify the two.
+getAllContext :: Context -> M.Map Atom Kind
+getAllContext c = c ^. context <> c ^. addContext
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs
index 6a5ecea8..e0132f16 100644
--- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs
@@ -16,93 +16,35 @@ module LambdaBuffers.Compiler.KindCheck.Inference (
 
 import Data.Bifunctor (Bifunctor (second))
 
+import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext, context, getAllContext)
+import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KVar, Type, (:->:)))
+import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var))
+import LambdaBuffers.Compiler.KindCheck.Variable (Atom)
+
 import Control.Monad.Freer (Eff, Member, Members, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
 import Control.Monad.Freer.Reader (Reader, ask, asks, local, runReader)
 import Control.Monad.Freer.State (State, evalState, get, put)
 import Control.Monad.Freer.Writer (Writer, runWriter, tell)
 
-import Control.Lens (Getter, makeLenses, to, (&), (.~), (^.))
+import Data.String (fromString)
+import Data.Text qualified as T
+
+import Control.Lens (Getter, to, (&), (.~), (^.))
+import Data.Map qualified as M
 
 import Prettyprinter (
   Doc,
   Pretty (pretty),
-  braces,
-  comma,
   encloseSep,
   hang,
-  hsep,
   lbracket,
   line,
-  parens,
-  punctuate,
   rbracket,
   space,
   (<+>),
  )
 
-type Atom = String
-type Var = String
-
-infixr 8 :->:
-
-data Kind
-  = Type
-  | Kind :->: Kind
-  | KVar Atom
-  deriving stock (Eq, Show)
-
-instance Pretty Kind where
-  pretty = \case
-    Type -> "*"
-    ((x :->: y) :->: z) -> parens (pretty $ x :->: y) <+> "→" <+> pretty z
-    x :->: y -> pretty x <+> "→" <+> pretty y
-    KVar a -> pretty a
-
-data Type
-  = Var Var
-  | App Type Type
-  | Abs String Type
-  deriving stock (Eq, Show)
-
-instance Pretty Type where
-  pretty = \case
-    Var a -> pretty a
-    App t1 t2 -> show' t1 <> " " <> show' t2
-    Abs a t1 -> "λ" <> pretty a <> "." <> pretty t1
-    where
-      show' :: Type -> Doc ann
-      show' = \case
-        Var a -> pretty a
-        App t1 t2 -> parens $ show' t1 <+> show' t2
-        Abs a t1 -> parens $ "λ" <> pretty a <> "." <> show' t1
-
-data Context = Context
-  { _context :: [(Atom, Kind)]
-  , _addContext :: [(Atom, Kind)]
-  }
-  deriving stock (Show, Eq)
-
-makeLenses ''Context
-
-instance Pretty Context where
-  pretty c = case c ^. addContext of
-    [] -> "Γ"
-    ctx -> "Γ" <+> "∪" <+> braces (setPretty ctx)
-    where
-      setPretty :: [(Atom, Kind)] -> Doc ann
-      setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
-
-instance Semigroup Context where
-  (Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2)
-
-instance Monoid Context where
-  mempty = Context mempty mempty
-
--- | Utility to unify the two.
-getAllContext :: Context -> [(Atom, Kind)]
-getAllContext c = c ^. context <> c ^. addContext
-
 newtype Judgement = Judgement {getJudgement :: (Context, Type, Kind)}
   deriving stock (Show, Eq)
 
@@ -125,11 +67,11 @@ instance Pretty Derivation where
       dNest j ds = pretty j <> line <> hang 2 (encloseSep (lbracket <> space) rbracket (space <> "∧" <> space) (pretty <$> ds))
 
 data InferErr
-  = Misc String
-  | ImpossibleErr String
-  | UnboundTermErr String
-  | ImpossibleUnificationErr String
-  | RecursiveSubstitutionErr String
+  = Misc T.Text
+  | ImpossibleErr T.Text
+  | UnboundTermErr T.Text
+  | ImpossibleUnificationErr T.Text
+  | RecursiveSubstitutionErr T.Text
   deriving stock (Show, Eq)
 
 newtype Constraint = Constraint (Kind, Kind)
@@ -180,11 +122,12 @@ infer ctx t = do
     defTerms =
       mempty
         & context
-          .~ [ ("Either", Type :->: Type :->: Type)
-             , ("()", Type)
-             , ("Void", Type)
-             , ("(,)", Type :->: Type :->: Type)
-             ]
+          .~ M.fromList
+            [ ("Σ", Type :->: Type :->: Type)
+            , ("Π", Type :->: Type :->: Type)
+            , ("𝟙", Type)
+            , ("𝟘", Type)
+            ]
 
 --------------------------------------------------------------------------------
 -- Implementation
@@ -207,7 +150,7 @@ derive x = do
       pure $ Application (Judgement (c, x, v)) d1 d2
     Abs v t -> do
       newTy <- KVar <$> fresh
-      d <- local (\(Context ctx addC) -> Context ctx $ (v, newTy) : addC) (derive t)
+      d <- local (\(Context ctx addC) -> Context ctx $ M.insert v newTy addC) (derive t)
       let ty = d ^. topKind
       freshT <- KVar <$> fresh
       tell [Constraint (freshT, newTy :->: ty)]
@@ -226,9 +169,9 @@ derive x = do
 getBinding :: Atom -> Derive Kind
 getBinding t = do
   ctx <- asks getAllContext
-  case t `lookup` ctx of
+  case ctx M.!? t of
     Just x -> pure x
-    Nothing -> throwError $ UnboundTermErr $ show (pretty t)
+    Nothing -> throwError $ UnboundTermErr $ (T.pack . show . pretty) t
 
 -- | Gets kind from a derivation.
 topKind :: Getter Derivation Kind
@@ -284,21 +227,21 @@ unify (constraint@(Constraint (l, r)) : xs) = case l of
     _ -> unify $ Constraint (r, l) : xs
   where
     nope :: forall eff b a. (Member (Error InferErr) eff, Pretty b) => b -> Eff eff a
-    nope c = throwError $ ImpossibleUnificationErr $ unlines ["Cannot unify: " <> show (pretty c)]
+    nope c = throwError . ImpossibleUnificationErr . T.unlines $ ["Cannot unify: " <> (T.pack . show . pretty) c]
 
-    appearsErr :: forall eff a. Member (Error InferErr) eff => String -> Kind -> Eff eff a
+    appearsErr :: forall eff a. Member (Error InferErr) eff => T.Text -> Kind -> Eff eff a
     appearsErr var ty =
       throwError $
         RecursiveSubstitutionErr $
           mconcat
             [ "Cannot unify: "
-            , show (pretty var)
+            , T.pack . show . pretty $ var
             , " with "
-            , show (pretty ty)
+            , T.pack . show . pretty $ ty
             , ". "
-            , show (pretty var)
+            , T.pack . show . pretty $ var
             , " appears in: "
-            , show (pretty ty)
+            , T.pack . show . pretty $ ty
             , "."
             ]
 
@@ -329,12 +272,12 @@ substitute s d = case d of
   where
     applySubsToJudgement sub (Judgement (ctx, t, k)) = Judgement (applySubstitutionCtx s ctx, t, applySubstitution sub k)
 
-    applySubstitutionCtx subs c@(Context ctx addCtx) = case addCtx of
+    applySubstitutionCtx subs c@(Context ctx addCtx) = case M.toList addCtx of
       [] -> c
-      xs -> Context ctx $ second (applySubstitution subs) <$> xs
+      xs -> Context ctx $ M.fromList $ second (applySubstitution subs) <$> xs
 
 -- :fixme: not avoiding any clashes
 
 -- | Fresh atoms
 atoms :: [Atom]
-atoms = ['1' ..] >>= \y -> ['a' .. 'z'] >>= \x -> pure [x, y]
+atoms = ['1' ..] >>= \y -> ['a' .. 'z'] >>= \x -> pure . fromString $ [x, y]
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs
new file mode 100644
index 00000000..fb86df9d
--- /dev/null
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs
@@ -0,0 +1,19 @@
+module LambdaBuffers.Compiler.KindCheck.Kind (Kind (Type, (:->:), KVar)) where
+
+import LambdaBuffers.Compiler.KindCheck.Variable (Atom)
+import Prettyprinter (Pretty (pretty), parens, (<+>))
+
+infixr 8 :->:
+
+data Kind
+  = Type
+  | Kind :->: Kind
+  | KVar Atom
+  deriving stock (Eq, Show)
+
+instance Pretty Kind where
+  pretty = \case
+    Type -> "*"
+    ((x :->: y) :->: z) -> parens (pretty $ x :->: y) <+> "→" <+> pretty z
+    x :->: y -> pretty x <+> "→" <+> pretty y
+    KVar a -> pretty a
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs
new file mode 100644
index 00000000..edf693d5
--- /dev/null
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs
@@ -0,0 +1,22 @@
+module LambdaBuffers.Compiler.KindCheck.Type (Type (Var, Abs, App)) where
+
+import LambdaBuffers.Compiler.KindCheck.Variable (Var)
+import Prettyprinter (Doc, Pretty (pretty), parens, (<+>))
+
+data Type
+  = Var Var
+  | App Type Type
+  | Abs Var Type
+  deriving stock (Eq, Show)
+
+instance Pretty Type where
+  pretty = \case
+    Var a -> pretty a
+    App t1 t2 -> show' t1 <> " " <> show' t2
+    Abs a t1 -> "λ" <> pretty a <> "." <> pretty t1
+    where
+      show' :: Type -> Doc ann
+      show' = \case
+        Var a -> pretty a
+        App t1 t2 -> parens $ show' t1 <+> show' t2
+        Abs a t1 -> parens $ "λ" <> pretty a <> "." <> show' t1
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Variable.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Variable.hs
new file mode 100644
index 00000000..7dbcd2f6
--- /dev/null
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Variable.hs
@@ -0,0 +1,6 @@
+module LambdaBuffers.Compiler.KindCheck.Variable (Atom, Var) where
+
+import Data.Text (Text)
+
+type Atom = Text
+type Var = Text
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs
index d303a001..c6a75c98 100644
--- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs
@@ -1,7 +1,12 @@
 {-# LANGUAGE OverloadedLabels #-}
+{-# OPTIONS_GHC -Wno-missing-import-lists #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
-module LambdaBuffers.Compiler.ProtoCompat (IsMessage (..), FromProtoErr (..), ProtoError (..)) where
+module LambdaBuffers.Compiler.ProtoCompat (IsMessage (..), FromProtoErr (..), ProtoError (..), module X) where
+
+-- NOTE(cstml): I'm re-exporting the module from here as it makes more sense -
+-- also avoids annoying errors.
+import LambdaBuffers.Compiler.ProtoCompat.Types as X
 
 import Control.Lens (Getter, to, (&), (.~), (^.))
 import Data.Foldable (toList)
@@ -16,41 +21,6 @@ import Proto.Compiler_Fields qualified as P
 
 import Data.Text qualified as Text
 import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkTyName, checkVarName)
-import LambdaBuffers.Compiler.ProtoCompat.Types (
-  ClassDef (ClassDef),
-  ClassName (ClassName),
-  CompilerInput (CompilerInput),
-  ConstrName (ConstrName),
-  Constraint (Constraint),
-  Constructor (Constructor),
-  Field (Field),
-  FieldName (FieldName),
-  ForeignRef (ForeignRef),
-  InstanceClause (InstanceClause),
-  Kind (Kind),
-  KindRefType (KType, KUnspecified),
-  KindType (KindArrow, KindRef),
-  LocalRef (LocalRef),
-  Module (Module),
-  ModuleName (ModuleName),
-  ModuleNamePart (ModuleNamePart),
-  Product (RecordI, TupleI),
-  Record (Record),
-  SourceInfo (SourceInfo),
-  SourcePosition (SourcePosition),
-  Sum (Sum),
-  Tuple (Tuple),
-  Ty (TyAppI, TyRefI, TyVarI),
-  TyAbs (TyAbs),
-  TyApp (TyApp),
-  TyArg (TyArg),
-  TyBody (OpaqueI, SumI),
-  TyDef (TyDef),
-  TyName (TyName),
-  TyRef (ForeignI, LocalI),
-  TyVar (TyVar),
-  VarName (VarName),
- )
 import Proto.Compiler (NamingError)
 
 note :: e -> Maybe a -> Either e a
diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs
index 9c7cdcc4..d446d4e8 100644
--- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs
+++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs
@@ -79,10 +79,7 @@ data FieldName = FieldName {name :: Text, sourceInfo :: SourceInfo}
 data ClassName = ClassName {name :: Text, sourceInfo :: SourceInfo}
   deriving stock (Show, Eq, Ord, Generic)
 
-data Kind = Kind
-  { kind :: KindType
-  , sourceInfo :: SourceInfo
-  }
+data Kind = Kind {kind :: KindType, sourceInfo :: SourceInfo}
   deriving stock (Show, Eq, Ord, Generic)
 
 data KindType
@@ -95,10 +92,7 @@ data KindRefType
   | KType
   deriving stock (Show, Eq, Ord, Generic)
 
-data TyVar = TyVar
-  { varName :: VarName
-  , sourceInfo :: SourceInfo
-  }
+data TyVar = TyVar {varName :: VarName, sourceInfo :: SourceInfo}
   deriving stock (Show, Eq, Ord, Generic)
 
 data Ty
@@ -121,10 +115,7 @@ data ForeignRef = ForeignRef
   }
   deriving stock (Show, Eq, Ord, Generic)
 
-data LocalRef = LocalRef
-  { tyName :: TyName
-  , sourceInfo :: SourceInfo
-  }
+data LocalRef = LocalRef {tyName :: TyName, sourceInfo :: SourceInfo}
   deriving stock (Show, Eq, Ord, Generic)
 
 data TyRef
@@ -228,3 +219,4 @@ data Module = Module
 
 newtype CompilerInput = CompilerInput {modules :: [Module]}
   deriving stock (Show, Eq, Ord, Generic)
+  deriving newtype (Monoid, Semigroup)
diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs
index d445da27..b214f688 100644
--- a/lambda-buffers-compiler/test/Test/KindCheck.hs
+++ b/lambda-buffers-compiler/test/Test/KindCheck.hs
@@ -1,98 +1,213 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
 module Test.KindCheck (test) where
 
+import Control.Lens ((%~), (&), (.~))
+import Data.List.NonEmpty (NonEmpty ((:|)), cons)
 import LambdaBuffers.Compiler.KindCheck (
-  KindCheckFailure (InferenceFailed),
-  TypeDefinition (TypeDefinition, _td'name, _td'sop, _td'variables),
-  kindCheckType,
-  runKindCheckEff,
- )
-import LambdaBuffers.Compiler.KindCheck.Inference (
-  InferErr (ImpossibleUnificationErr),
-  Kind (Type, (:->:)),
-  Type (Abs, App, Var),
+  check,
+  foldWithProduct,
+  foldWithSum,
  )
+import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var))
+import LambdaBuffers.Compiler.ProtoCompat qualified as P
 import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.HUnit (testCase, (@?=))
+import Test.Tasty.HUnit (assertBool, testCase, (@?=))
 
 test :: TestTree
-test = testGroup "KindChecker tests" [t1, t2, t3, t4, t5]
-
-runKC :: [TypeDefinition] -> Either KindCheckFailure [Kind]
-runKC = runKindCheckEff . kindCheckType
-
-t1 :: TestTree
-t1 =
-  testCase "No Definition, No Kinds" $
-    runKC [] @?= Right []
-
-t2 :: TestTree
-t2 =
-  testCase "Maybe has the correct Kind" $
-    runKC [tdMaybe] @?= Right [Type :->: Type]
-
-t3 :: TestTree
-t3 =
-  testCase "Maybe works correctly when used as a type" $
-    runKC [tdT1, tdMaybe] @?= Right [Type :->: Type, Type :->: Type]
-
-t4 :: TestTree
-t4 =
-  testCase "Maybe and a term containing a maybe work correctly" $
-    runKC [tdT1, tdMaybe, tdT2] @?= Right [Type :->: Type, Type :->: Type, Type :->: Type]
-
-t5 :: TestTree
-t5 =
-  testCase "Bad Type is caught and reported" $
-    runKC [tdMaybe, tdBT0]
-      @?= Left
-        ( InferenceFailed
-            ( TypeDefinition
-                { _td'name = "T"
-                , _td'variables = []
-                , _td'sop = App (Var "Maybe") (Var "Maybe")
-                }
-            )
-            (ImpossibleUnificationErr "Cannot unify: * = * \8594 *\n")
-        )
+test = testGroup "Compiler tests" [testCheck, testFolds]
 
 --------------------------------------------------------------------------------
--- Manual type definitions.
-
-tdMaybe :: TypeDefinition
-tdMaybe =
-  TypeDefinition
-    { _td'name = "Maybe"
-    , _td'variables = ["a"]
-    , _td'sop =
-        Abs "a" $
-          App
-            (App (Var "Either") (Var "()"))
-            (Var "a")
-    }
+-- Module tests
 
--- T1 ~ T a = T Maybe (Maybe a)
-tdT1 :: TypeDefinition
-tdT1 =
-  TypeDefinition
-    { _td'name = "T"
-    , _td'variables = ["b"]
-    , _td'sop = Abs "b" $ App (Var "Maybe") (App (Var "Maybe") (Var "b"))
-    }
+testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFailing]
 
--- T2 ~ T a = T Maybe (Maybe a)
-tdT2 :: TypeDefinition
-tdT2 =
-  TypeDefinition
-    { _td'name = "T2"
-    , _td'variables = ["a"]
-    , _td'sop = Abs "a" $ App (Var "T") (App (Var "Maybe") (Var "a"))
-    }
+trivialKCTest =
+  testCase "Empty CompInput should check." $
+    check (P.CompilerInput []) @?= Right ()
 
--- T2 ~ T = T Maybe Maybe
-tdBT0 :: TypeDefinition
-tdBT0 =
-  TypeDefinition
-    { _td'name = "T"
-    , _td'variables = []
-    , _td'sop = App (Var "Maybe") (Var "Maybe")
+kcTestMaybe =
+  testCase "Maybe should pass." $
+    check ci1 @?= Right ()
+
+kcTestFailing =
+  testCase "This should fail." $
+    assertBool "Test should have failed." $
+      check ci2 /= Right ()
+
+esi = P.SourceInfo "Empty Info" (P.SourcePosition 0 0) (P.SourcePosition 0 1)
+
+modMaybe =
+  P.Module
+    { P.moduleName =
+        P.ModuleName
+          { P.parts = [P.ModuleNamePart "Module" esi]
+          , P.sourceInfo = esi
+          }
+    , P.typeDefs =
+        [ P.TyDef
+            { P.tyName = P.TyName "Maybe" esi
+            , P.tyAbs =
+                P.TyAbs
+                  { P.tyArgs =
+                      [ P.TyArg
+                          { P.argName = P.VarName "a" esi
+                          , P.argKind =
+                              P.Kind
+                                { P.kind = P.KindRef P.KType
+                                , P.sourceInfo = esi
+                                }
+                          , P.sourceInfo = esi
+                          }
+                      ]
+                  , P.tyBody =
+                      P.SumI $
+                        P.Sum
+                          { constructors =
+                              P.Constructor
+                                { P.constrName = P.ConstrName {P.name = "Nothing", P.sourceInfo = esi}
+                                , P.product = P.TupleI $ P.Tuple {P.fields = [], P.sourceInfo = esi}
+                                }
+                                :| [ P.Constructor
+                                      { P.constrName = P.ConstrName {P.name = "Just", P.sourceInfo = esi}
+                                      , P.product =
+                                          P.TupleI $
+                                            P.Tuple
+                                              { P.fields =
+                                                  [ P.TyVarI
+                                                      ( P.TyVar
+                                                          { P.varName =
+                                                              P.VarName
+                                                                { P.name = "a"
+                                                                , P.sourceInfo = esi
+                                                                }
+                                                          , P.sourceInfo = esi
+                                                          }
+                                                      )
+                                                  ]
+                                              , P.sourceInfo = esi
+                                              }
+                                      }
+                                   ]
+                          , sourceInfo = esi
+                          }
+                  , P.sourceInfo = esi
+                  }
+            , P.sourceInfo = esi
+            }
+        ]
+    , P.classDefs = mempty
+    , P.instances = mempty
+    , P.sourceInfo = esi
     }
+
+ci1 :: P.CompilerInput
+ci1 = P.CompilerInput {P.modules = [modMaybe]}
+
+{- | Maybe = ...
+   B a = B Maybe
+
+ Should fail as B a defaults to B :: Type -> Type and Maybe is inferred as
+ Type -> Type. This is an inconsistency failure.
+-}
+ci2 = ci1 & #modules .~ [addMod]
+  where
+    addMod =
+      modMaybe
+        & #typeDefs
+          %~ ( <>
+                [ -- B a = B Maybe
+                  P.TyDef
+                    { P.tyName = P.TyName "B" esi
+                    , P.tyAbs =
+                        P.TyAbs
+                          { P.tyArgs =
+                              [ P.TyArg
+                                  { P.argName = P.VarName "a" esi
+                                  , P.argKind =
+                                      P.Kind
+                                        { P.kind = P.KindRef P.KType
+                                        , P.sourceInfo = esi
+                                        }
+                                  , P.sourceInfo = esi
+                                  }
+                              ]
+                          , P.tyBody =
+                              P.SumI $
+                                P.Sum
+                                  { constructors =
+                                      P.Constructor
+                                        { P.constrName = P.ConstrName {P.name = "B", P.sourceInfo = esi}
+                                        , P.product =
+                                            P.TupleI $
+                                              P.Tuple
+                                                { P.fields =
+                                                    [ P.TyRefI $
+                                                        P.LocalI $
+                                                          P.LocalRef
+                                                            { P.tyName = P.TyName {P.name = "Maybe", P.sourceInfo = esi}
+                                                            , P.sourceInfo = esi
+                                                            }
+                                                    ]
+                                                , P.sourceInfo = esi
+                                                }
+                                        }
+                                        :| []
+                                  , sourceInfo = esi
+                                  }
+                          , P.sourceInfo = esi
+                          }
+                    , P.sourceInfo = esi
+                    }
+                ]
+             )
+
+--------------------------------------------------------------------------------
+-- Fold tests
+
+testFolds =
+  testGroup
+    "Test Folds"
+    [ testGroup "Test Product Folds." [testFoldProd1, testFoldProd2, testFoldProd3]
+    , testGroup "Test Sum Folds." [testSumFold1, testSumFold2, testSumFold3]
+    ]
+
+-- | [ a ] -> a
+testFoldProd1 =
+  testCase "Fold with product - 1 type." $
+    foldWithProduct (Var "a" :| []) @?= Var "a"
+
+-- | [a ,b] -> (a,b)
+testFoldProd2 =
+  testCase "Fold with product - 2 types." $
+    foldWithProduct (cons (Var "b") $ Var "a" :| [])
+      @?= App (App (Var "Π") (Var "b")) (Var "a")
+
+-- | [ a, b ,c ] -> (a,(b,c))
+testFoldProd3 =
+  testCase "Fold with product - 2 types." $
+    foldWithProduct (cons (Var "c") $ cons (Var "b") $ Var "a" :| [])
+      @?= App
+        (App (Var "Π") (Var "c"))
+        (App (App (Var "Π") (Var "b")) (Var "a"))
+
+-- | [ a ] -> a
+testSumFold1 =
+  testCase "Fold 1 type." $
+    foldWithSum (Var "a" :| []) @?= Var "a"
+
+-- | [ a , b ] -> a | b
+testSumFold2 =
+  testCase "Fold 2 type." $
+    foldWithSum (cons (Var "b") $ Var "a" :| [])
+      @?= App (App (Var "Σ") (Var "b")) (Var "a")
+
+-- | [ a , b , c ] -> a | ( b | c )
+testSumFold3 =
+  testCase "Fold 3 types." $
+    foldWithSum (cons (Var "c") $ cons (Var "b") $ Var "a" :| [])
+      @?= App
+        (App (Var "Σ") (Var "c"))
+        (App (App (Var "Σ") (Var "b")) (Var "a"))