Typechecker rewrite

gcl/gcl.cabal

@@ -30,6 +30,7 @@ library
       GCL.Range
       GCL.Substitution
       GCL.Type
+      GCL.Type2.Common
       GCL.Type2.Infer
       GCL.Type2.MiniAst
       GCL.Type2.RSE

gcl/src/GCL/Type2/Common.hs

@@ -0,0 +1,15 @@
+module GCL.Type2.Common where
+
+import Data.Map (Map)
+import qualified Syntax.Abstract.Types as A
+import Syntax.Common.Types (Name)
+
+type TyVar = Name
+
+type TmVar = Name
+
+data Scheme
+  = Forall [TyVar] A.Type -- ∀α₁, ..., αₙ. t
+  deriving (Eq, Show)
+
+type Env = Map TmVar Scheme

gcl/src/GCL/Type2/Infer.hs

@@ -18,6 +18,7 @@ import qualified Data.Text as Text
 import Debug.Trace
 import GCL.Range (MaybeRanged (maybeRangeOf), Range)
 import GCL.Type (TypeError (..))
+import GCL.Type2.Common (Env, Scheme (..), TyVar)
 import GCL.Type2.RSE
 import qualified Hack
 import Pretty
@@ -30,16 +31,6 @@ newtype Inference = Inference
   { _counter :: Int
   }
 
-type TyVar = Name
-
-type TmVar = Name
-
-data Scheme
-  = Forall [TyVar] A.Type -- ∀α₁, ..., αₙ. t
-  deriving (Show)
-
-type Env = Map TmVar Scheme
-
 instance {-# OVERLAPPING #-} Show Env where
   show e = intercalate "\n" $ map (\(var, scheme) -> s var <> " :: " <> showScheme scheme) (Map.toList e)
     where
@@ -73,7 +64,6 @@ checkDuplicateNames names =
 checkOccurs :: Name -> A.Type -> Bool
 checkOccurs name ty = Set.member name (freeTypeVars ty)
 
--- TODO: maybe `Subst` type class?
 applySubst :: Subst -> A.Type -> A.Type
 applySubst _ ty@A.TBase {} = ty
 applySubst subst (A.TArray interval ty range) =
@@ -112,11 +102,11 @@ applySubstExpr subst (T.Op op ty) = T.Op op (applySubst subst ty)
 applySubstExpr subst (T.Chain chain) = T.Chain (applySubstChain subst chain)
 applySubstExpr subst (T.App e1 e2 range) = T.App (applySubstExpr subst e1) (applySubstExpr subst e2) range
 applySubstExpr subst (T.Lam param ty body range) = T.Lam param (applySubst subst ty) (applySubstExpr subst body) range
-applySubstExpr subst (T.Quant _ _ _ _ _) = undefined
+applySubstExpr subst (T.Quant op args cond expr range) = T.Quant (applySubstExpr subst op) args (applySubstExpr subst cond) (applySubstExpr subst expr) range
 applySubstExpr subst (T.ArrIdx arr index range) = T.ArrIdx (applySubstExpr subst arr) (applySubstExpr subst index) range
 applySubstExpr subst (T.ArrUpd arr index expr range) = T.ArrUpd (applySubstExpr subst arr) (applySubstExpr subst index) (applySubstExpr subst expr) range
 applySubstExpr subst (T.Case expr clauses range) = T.Case (applySubstExpr subst expr) (map (applySubstClause subst) clauses) range
-applySubstExpr subst (T.Subst _ _) = undefined
+applySubstExpr subst (T.Subst _ _) = undefined -- XXX: what is this?
 applySubstExpr subst (T.EHole text range ty holeNumber) = T.EHole text range (applySubst subst ty) holeNumber
 
 applySubstChain :: Subst -> T.Chain -> T.Chain
@@ -183,25 +173,28 @@ freeTypeVarsScheme (Forall tvs ty) =
 
 unify :: A.Type -> A.Type -> Maybe Range -> Result Subst
 unify (A.TBase t1 _) (A.TBase t2 _) _ | t1 == t2 = return mempty
-unify (A.TArray _i1 t1 _) (A.TArray _i2 t2 _) l = unify t1 t2 l
-unify (A.TArray _i t1 _) (A.TApp (A.TApp (A.TOp (Arrow _)) i _) t2 _) l = do
-  s1 <- unify i typeInt l
-  s2 <- unify t1 t2 l
+unify (A.TArray _i1 t1 _) (A.TArray _i2 t2 _) r = unify t1 t2 r
+unify (A.TArray _i t1 _) (A.TApp (A.TApp (A.TOp (Arrow _)) i _) t2 _) r = do
+  s1 <- unify i typeInt r
+  s2 <- unify t1 t2 r
   return (s2 <> s1)
-unify (A.TOp op1) (A.TOp op2) _ | op1 == op2 = return mempty
-unify (A.TData n1 l1) (A.TData n2 l2) _ = undefined
-unify (A.TApp a1 a2 _) (A.TApp b1 b2 _) l = do
-  s1 <- unify a1 b1 l
-  s2 <- unify (applySubst s1 a2) (applySubst s1 b2) l
+unify (A.TOp (Arrow _)) (A.TOp (Arrow _)) _ = return mempty
+unify t1@(A.TData n1 _) t2@(A.TData n2 _) r =
+  if n1 == n2
+    then return mempty
+    else throwError $ UnifyFailed t1 t2 r
+unify (A.TApp a1 a2 _) (A.TApp b1 b2 _) r = do
+  s1 <- unify a1 b1 r
+  s2 <- unify (applySubst s1 a2) (applySubst s1 b2) r
   return $ s2 <> s1
-unify (A.TVar name _) ty l = unifyVar name ty l
-unify ty (A.TVar name _) l = unifyVar name ty l
+unify (A.TVar name _) ty r = unifyVar name ty r
+unify ty (A.TVar name _) r = unifyVar name ty r
 unify A.TType A.TType _ = return mempty
-unify t1 t2 l =
+unify t1 t2 r =
   trace
     (show (pretty t1) <> " != " <> show (pretty t2))
     throwError
-    $ UnifyFailed t1 t2 l
+    $ UnifyFailed t1 t2 r
 
 unifyVar :: Name -> A.Type -> Maybe Range -> Result Subst
 unifyVar name ty range
@@ -211,11 +204,6 @@ unifyVar name ty range
       let subst = Map.singleton name ty
        in return subst
 
--- (-->) :: a -> b -> (a --> b)
---
-
--- * -> *
-
 typeToKind :: A.Type -> RSE Env Inference A.Type
 typeToKind A.TBase {} = return A.TType
 typeToKind A.TArray {} = return $ A.TType `typeToType` A.TType
@@ -227,35 +215,24 @@ typeToKind (A.TData name _) = do
   case Map.lookup name env of
     Just (Forall _ k) -> return k
     Nothing -> throwError $ NotInScope name
-typeToKind (A.TVar name _) = do
-  env <- ask
-  case Map.lookup name env of
-    -- BUG: this probably wrong
-    Just (Forall tyParams _) -> return $ foldr (\_ acc -> A.TType `typeToType` acc) A.TType tyParams -- XXX: is this correct?
-    Nothing -> throwError $ NotInScope name
-typeToKind A.TMetaVar {} = undefined
+typeToKind (A.TVar _ _) = do
+  return A.TType
+typeToKind (A.TMetaVar name range) = typeToKind (A.TVar name range) -- XXX: hack
 typeToKind A.TType = return A.TType
 typeToKind (A.TApp t1 t2 _) = do
   t1Kind <- typeToKind t1
-  -- BUG: this is wrong, didn't even check k2
+  t2Kind <- typeToKind t2
   case t1Kind of
     (A.TApp (A.TApp (A.TOp (Arrow _)) k1 _) k2 _) -> do
-      _ <- lift $ unify t2 k1 (maybeRangeOf t2)
+      _ <- lift $ unify t2Kind k1 (maybeRangeOf t2)
       return k2
-    (A.TApp A.TType _ range) -> throwError $ PatternArityMismatch 2 1 range
-    -- \* *
-    (A.TApp _ (A.TApp _ _ _) range) -> throwError $ PatternArityMismatch 1 2 range -- (* -> *) (* -> *)
+    A.TType -> do
+      -- \* *
+      throwError $ UnifyFailed A.TType t2Kind (maybeRangeOf t1)
     ty' -> do
       traceM $ show ty'
       error "unknown kind"
 
--- typeToKind (TApp f x) = do
---  (k1 -> k2) <- typeToKind f
---  typeToKind x == k1
---  return k2
-
--- (* -> * -> *) (* -> *)
-
 -- we keep `T.Expr` to prevent repeating calculate the same expression
 infer :: A.Expr -> RSE Env Inference (Subst, A.Type, T.Expr)
 infer (A.Lit lit range) = inferLit lit range