add a type map to type checker and prune types in unification

src/Data/Abstract/Type.hs

@@ -1,14 +1,15 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, TypeOperators, UndecidableInstances, LambdaCase #-}
 module Data.Abstract.Type
   ( Type (..)
   , TypeError (..)
-  , runTypeError
+  , runTypes
   , unify
   ) where
 
 import Control.Abstract
 import Data.Abstract.Environment as Env
 import Data.Semigroup.Foldable (foldMap1)
+import qualified Data.Map as Map
 import Prologue hiding (TypeError)
 
 type TName = Int
@@ -67,28 +68,75 @@ instance Eq1   TypeError where liftEq      _ (UnificationError a1 b1) (Unificati
 instance Ord1  TypeError where liftCompare _ (UnificationError a1 b1) (UnificationError a2 b2) = compare a1 a2 <> compare b1 b2
 instance Show1 TypeError where liftShowsPrec _ _ = showsPrec
 
-
 runTypeError :: Effectful m => m (Resumable TypeError ': effects) a -> m effects (Either (SomeExc TypeError) a)
 runTypeError = runResumable
 
+runTypeMap :: ( Effectful m
+              , Monad (m effects)
+              )
+           => m (State TypeMap ': effects) a
+           -> m effects a
+runTypeMap = runState emptyTypeMap >=> pure . fst
 
+runTypes :: ( Effectful m
+            , Monad (m effects)
+            )
+         => m (Resumable TypeError ': State TypeMap ': effects) a
+         -> m effects (Either (SomeExc TypeError) a)
+runTypes = runTypeMap . runTypeError
+
+newtype TypeMap = TypeMap { unTypeMap :: Map.Map TName Type }
+
+emptyTypeMap :: TypeMap
+emptyTypeMap = TypeMap Map.empty
+
+modifyTypeMap :: ( Effectful m
+                 , Member (State TypeMap) effects
+                 )
+              => (Map.Map TName Type -> Map.Map TName Type)
+              -> m effects ()
+modifyTypeMap f = modify (TypeMap . f . unTypeMap)
+
+prune :: ( Effectful m
+         , Monad (m effects)
+         , Member (State TypeMap) effects
+         )
+      => Type
+      -> m effects Type
+prune (Var id) = Map.lookup id . unTypeMap <$> get >>= \case
+                    Just ty -> do
+                      pruned <- prune ty
+                      modifyTypeMap (Map.insert id pruned)
+                      pure pruned
+                    Nothing -> pure (Var id)
+prune ty = pure ty
 
 -- | Unify two 'Type's.
-unify :: (Effectful m, Applicative (m effects), Member (Resumable TypeError) effects) => Type -> Type -> m effects Type
-unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
-unify a Null = pure a
-unify Null b = pure b
--- FIXME: this should be constructing a substitution.
-unify (Var _) b = pure b
-unify a (Var _) = pure a
-unify (Array t1) (Array t2) = Array <$> unify t1 t2
--- FIXME: unifying with sums should distribute nondeterministically.
--- FIXME: ordering shouldn’t be significant for undiscriminated sums.
-unify (a1 :+ b1) (a2 :+ b2) = (:+) <$> unify a1 a2 <*> unify b1 b2
-unify (a1 :* b1) (a2 :* b2) = (:*) <$> unify a1 a2 <*> unify b1 b2
-unify t1 t2
-  | t1 == t2  = pure t2
-  | otherwise = throwResumable (UnificationError t1 t2)
+unify :: ( Effectful m
+         , Monad (m effects)
+         , Member (Resumable TypeError) effects
+         , Member (State TypeMap) effects
+         )
+      => Type
+      -> Type
+      -> m effects Type
+unify a b = do
+  a' <- prune a
+  b' <- prune b
+  case (a', b') of
+    (a1 :-> b1, a2 :-> b2) -> (:->) <$> unify a1 a2 <*> unify b1 b2
+    (a, Null) -> pure a
+    (Null, b) -> pure b
+    -- FIXME: this should be constructing a substitution.
+    (Var _, b) -> pure b
+    (a, Var _) -> pure a
+    (Array t1, Array t2) -> Array <$> unify t1 t2
+  -- FIXME: unifying with sums should distribute nondeterministically.
+  -- FIXME: ordering shouldn’t be significant for undiscriminated sums.
+    (a1 :+ b1, a2 :+ b2) -> (:+) <$> unify a1 a2 <*> unify b1 b2
+    (a1 :* b1, a2 :* b2) -> (:*) <$> unify a1 a2 <*> unify b1 b2
+    (t1, t2) | t1 == t2 -> pure t2
+    _ -> throwResumable (UnificationError a b)
 
 instance Ord address => ValueRoots address Type where
   valueRoots _ = mempty
@@ -115,6 +163,7 @@ instance ( Member (Allocator address Type) effects
          , Member (Env address) effects
          , Member Fresh effects
          , Member (Resumable TypeError) effects
+         , Member (State TypeMap) effects
          , Member (Return address) effects
          )
       => AbstractFunction address Type effects where
@@ -142,6 +191,7 @@ instance ( Member (Allocator address Type) effects
          , Member Fresh effects
          , Member NonDet effects
          , Member (Resumable TypeError) effects
+         , Member (State TypeMap) effects
          , Member (Return address) effects
          )
       => AbstractValue address Type effects where

src/Semantic/Util.hs

@@ -87,7 +87,7 @@ checking
   . runEnvironmentError
   . runEvalError
   . runAddressError
-  . runTypeError
+  . runTypes
 
 evalGoProject         = justEvaluating <=< evaluateProject (Proxy :: Proxy 'Language.Go)         goParser         Language.Go
 evalRubyProject       = justEvaluating <=< evaluateProject (Proxy :: Proxy 'Language.Ruby)       rubyParser       Language.Ruby