Working implementation.

src/Analysis/Abstract/TypeChecking.hs

@@ -18,14 +18,30 @@ deriving instance MonadModuleTable location term value (m effects) => MonadModul
 deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (TypeChecking m effects)
 
 instance ( Effectful m
-         , MonadAnalysis location term Type (m effects)
-         , Member (Resumable (TypeError Type)) effects
-         , MonadValue location Type (TypeChecking m effects)
+         , Alternative (m effects)
+         , MonadAnalysis location term value (m effects)
+         , Member (Resumable TypeError) effects
+         , Member NonDet effects
+         , Member Fail effects
+         , MonadValue location value (TypeChecking m effects)
+         , value ~ Type
          )
-      => MonadAnalysis location term Type (TypeChecking m effects) where
+      => MonadAnalysis location term value (TypeChecking m effects) where
 
-  type Effects location term Type (TypeChecking m effects) = Resumable (TypeError Type) ': NonDet ': Effects location term Type (m effects)
+  type Effects location term value (TypeChecking m effects) = Resumable TypeError ': Effects location term value (m effects)
 
-  analyzeTerm eval term = resume @(TypeError Type) (liftAnalyze analyzeTerm eval term) (
-      \yield err -> case err of
-        NoValueError v -> yield "")
+  analyzeTerm eval term =
+    resume @TypeError (liftAnalyze analyzeTerm eval term) (
+        \yield err -> case err of
+          NoValueError _ a -> yield a
+          -- TODO: These should all yield both sides of the exception,
+          -- but something is mysteriously busted in the innards of typechecking,
+          -- so doing that just yields an empty list in the result type, which isn't
+          -- extraordinarily helpful. Better for now to just die with an error and
+          -- tackle this issue in a separate PR.
+          BitOpError{}       -> throwResumable err
+          NumOpError{}       -> throwResumable err
+          UnificationError{} -> throwResumable err
+        )
+
+  analyzeModule = liftAnalyze analyzeModule

src/Data/Abstract/Type.hs

@@ -36,14 +36,30 @@ data Type
 
 -- TODO: À la carte representation of types.
 
-data TypeError value resume where
-  NoValueError     :: value -> TypeError value resume
-  NumOpError       :: value -> value -> TypeError value resume
-  BitOpError       :: value -> value -> TypeError value resume
-  UnificationError :: value -> value -> TypeError value resume
+-- TODO: specialize these to type
+data TypeError resume where
+  NoValueError     :: Type -> a -> TypeError a
+  NumOpError       :: Type -> Type -> TypeError Type
+  BitOpError       :: Type -> Type -> TypeError Type
+  UnificationError :: Type -> Type -> TypeError Type
+
+deriving instance Show resume => Show (TypeError resume)
+
+instance Show1 TypeError where
+  liftShowsPrec _ _ _ (NoValueError v _)     = showString "NoValueError " . shows v
+  liftShowsPrec _ _ _ (NumOpError l r)       = showString "NumOpError " . shows [l, r]
+  liftShowsPrec _ _ _ (BitOpError l r)       = showString "BitOpError " . shows [l, r]
+  liftShowsPrec _ _ _ (UnificationError l r) = showString "UnificationError " . shows [l, r]
+
+instance Eq1 TypeError where
+  liftEq _ (NoValueError a _) (NoValueError b _)                       = a == b
+  -- liftEq _ (NamespaceError a) (NamespaceError b)                 = a == b
+  -- liftEq _ (ScopedEnvironmentError a) (ScopedEnvironmentError b) = a == b
+  -- liftEq _ (CallError a) (CallError b)                           = a == b
+  liftEq _ _             _                                       = False
 
 -- | Unify two 'Type's.
-unify :: MonadResume (TypeError Type) m => Type -> Type -> m Type
+unify :: MonadResume TypeError m => Type -> Type -> m Type
 unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
 unify a Null = pure a
 unify Null b = pure b
@@ -67,7 +83,7 @@ instance ( Alternative m
          , MonadFail m
          , MonadFresh m
          , MonadHeap location Type m
-         , MonadResume (TypeError Type) m
+         , MonadResume TypeError m
          , Reducer Type (Cell location Type)
          )
       => MonadValue location Type m where
@@ -101,9 +117,9 @@ instance ( Alternative m
 
   scopedEnvironment _ = pure mempty
 
-  asString _ = throwResumable (NoValueError String)
-  asPair _   = throwResumable (NoValueError (Product []))
-  asBool _   = throwResumable (NoValueError Bool)
+  asString _ = throwResumable (NoValueError String "")
+  asPair _   = throwResumable (NoValueError (Product []) (Hole, Hole))
+  asBool _   = throwResumable (NoValueError Bool True)
 
   isHole ty = pure (ty == Hole)
 

src/Semantic/Util.hs

@@ -6,6 +6,7 @@ module Semantic.Util where
 import           Analysis.Abstract.BadModuleResolutions
 import           Analysis.Abstract.BadValues
 import           Analysis.Abstract.BadVariables
+import           Analysis.Abstract.Caching
 import           Analysis.Abstract.Evaluating as X
 import           Analysis.Abstract.ImportGraph
 import           Analysis.Abstract.Quiet
@@ -47,7 +48,7 @@ import qualified Language.TypeScript.Assignment as TypeScript
 type JustEvaluating term = Evaluating (Located Precise term) term (Value (Located Precise term))
 type EvaluatingWithHoles term = BadModuleResolutions (BadVariables (BadValues (Quietly (Evaluating (Located Precise term) term (Value (Located Precise term))))))
 type ImportGraphingWithHoles term = ImportGraphing (EvaluatingWithHoles term)
-type Checking term = TypeChecking (EvaluatingWithHoles term)
+type Checking term = Caching (TypeChecking (Evaluating Monovariant term Type))
 
 evalGoProject path = runAnalysis @(JustEvaluating Go.Term) <$> evaluateProject goParser Nothing path
 evalRubyProject path = runAnalysis @(JustEvaluating Ruby.Term) <$> evaluateProject rubyParser rubyPrelude path
@@ -55,7 +56,7 @@ evalPHPProject path = runAnalysis @(JustEvaluating PHP.Term) <$> evaluateProject
 evalPythonProject path = runAnalysis @(JustEvaluating Python.Term) <$> evaluateProject pythonParser pythonPrelude path
 evalTypeScriptProject path = runAnalysis @(EvaluatingWithHoles TypeScript.Term) <$> evaluateProject typescriptParser Nothing path
 
-typecheckPythonFile path = runAnalysis @(Checking Python.Term) <$> evaluateProject pythonParser Nothing path
+typecheckGoFile path = runAnalysis @(Checking Go.Term) <$> evaluateProject goParser Nothing path
 
 rubyPrelude = Just $ File (TypeLevel.symbolVal (Proxy :: Proxy (PreludePath Ruby.Term))) (Just Language.Ruby)
 pythonPrelude = Just $ File (TypeLevel.symbolVal (Proxy :: Proxy (PreludePath Python.Term))) (Just Language.Python)