From 4aa72beccb1953a1ec47a59367a6ec1d7628837f Mon Sep 17 00:00:00 2001
From: Martin Fredin <fredin.martin@gmail.com>
Date: Fri, 5 May 2023 09:02:10 +0200
Subject: [PATCH] Add missing clauses. Still broken

---
 src/TypeChecker/TypeCheckerBidir.hs | 57 ++++++++++++++++-------------
 1 file changed, 31 insertions(+), 26 deletions(-)

diff --git a/src/TypeChecker/TypeCheckerBidir.hs b/src/TypeChecker/TypeCheckerBidir.hs
index fcef885..04a8d91 100644
--- a/src/TypeChecker/TypeCheckerBidir.hs
+++ b/src/TypeChecker/TypeCheckerBidir.hs
@@ -482,35 +482,37 @@ subtype (TEVar alpha) a | notElem alpha $ frees a = instantiateL alpha a
 --  Γ[ά] ⊢ A <: ά ⊣ Δ
 subtype a  (TEVar alpha) | notElem alpha $ frees a = instantiateR a alpha
 
-subtype t1 t2 = case (t1, t2) of
-    (TData name1 typs1, TData name2 typs2)
 
-      --  D₁ = D₂
-      --  ----------------
-      --  Γ ⊢ D₁ () <: D₂ ()
-      | name1 == name2
-      , [] <- typs1
-      , [] <- typs2
-      -> pure ()
+subtype (TData name1 typs1) (TData name2 typs2)
 
-      --                    Γ ⊢ ά₁ <: έ₁ ⊣ Θ₁
-      --                           ...
-      -- D₁ = D₂   Θₙ₋₁ ⊢ [Θₙ₋₁]άₙ <: [Θₙ₋₁]έₙ ⊣ Δ
-      -- -------------------------------------------
-      -- Γ ⊢ D (ά₁ ‥ άₙ) <: D (έ₁ ‥ έₙ) ⊣ Δ
-      | name1 == name2
-      , t1:t1s <- typs1
-      , t2:t2s <- typs2
-      -> do
-          subtype t1 t2
-          zipWithM_ go t1s t2s
-     where
-       go t1' t2' = do
-           t1'' <- apply t1'
-           t2'' <- apply t2'
-           subtype t1'' t2''
+    --  D₁ = D₂
+    --  ----------------
+    --  Γ ⊢ D₁ () <: D₂ ()
+    | name1 == name2
+    , [] <- typs1
+    , [] <- typs2
+    = pure ()
 
-    _ -> throwError $ unwords ["Types", ppT t1, "and", ppT t2, "doesn't match!"]
+    --                    Γ ⊢ ά₁ <: έ₁ ⊣ Θ₁
+    --                           ...
+    -- D₁ = D₂   Θₙ₋₁ ⊢ [Θₙ₋₁]άₙ <: [Θₙ₋₁]έₙ ⊣ Δ
+    -- -------------------------------------------
+    -- Γ ⊢ D (ά₁ ‥ άₙ) <: D (έ₁ ‥ έₙ) ⊣ Δ
+    | name1 == name2
+    , t1:t1s <- typs1
+    , t2:t2s <- typs2
+    = do
+    subtype t1 t2
+    zipWithM_ go t1s t2s
+  where
+    go t1' t2' = do
+        t1'' <- apply t1'
+        t2'' <- apply t2'
+        subtype t1'' t2''
+
+subtype (TIdent t1) (TIdent t2) | t1 == t2 = pure ()
+
+subtype t1 t2 = throwError $ unwords ["Types", show t1, "and", show t2, "doesn't match!"]
 
 ---------------------------------------------------------------------------
 -- * Instantiation rules
@@ -788,6 +790,7 @@ applyType' cxt typ | typ == typ' = typ'
         TFun t1 t2      -> on TFun (applyType' cxt) t1 t2
         -- [Γ](∀α. A) = (∀α. [Γ]A)
         TAll tvar t     -> TAll tvar $ applyType' cxt t
+        TIdent t        -> typ
 
 applyExp :: T.Exp' Type -> Tc (T.Exp' Type)
 applyExp exp = case exp of
@@ -841,6 +844,8 @@ ppT = \case
     TEVar (MkTEVar (LIdent s)) -> "tevar_" ++ s
     TData (UIdent name) typs   -> name ++ " (" ++ unwords (map ppT typs)
                                        ++ " )"
+    TIdent (UIdent name)       -> name
+
 ppEnvElem = \case
    EnvVar         (LIdent s) t           -> s ++ ":" ++ ppT t
    EnvTVar        (MkTVar  (LIdent s))   -> "tvar_" ++ s