filled in synthesize for let of binding that is a closed expression

parser-typechecker/src/Unison/ABT.hs

@@ -12,6 +12,7 @@
 module Unison.ABT where
 
 import Control.Applicative
+import Control.Monad
 import Data.List hiding (cycle)
 import Data.Maybe
 import Data.Ord
@@ -285,6 +286,25 @@ rebuildUp f (Term _ ann body) = case body of
   Abs x e -> abs' ann x (rebuildUp f e)
   Tm body -> tm' ann (f $ fmap (rebuildUp f) body)
 
+annotateBound :: (Ord v, Foldable f, Functor f) => Term f v a -> Term f v (a, Set v)
+annotateBound t = go Set.empty t where
+  go bound t = let a = (annotation t, bound) in case out t of
+    Var v -> annotatedVar a v
+    Cycle body -> cycle' a (go bound body)
+    Abs x body -> abs' a x (go (Set.insert x bound) body)
+    Tm body -> tm' a (go bound <$> body)
+
+foreachSubterm
+  :: (Traversable f, Applicative g, Ord v)
+  => (Term f v a -> g b)
+  -> Term f v a
+  -> g [b]
+foreachSubterm f e = case out e of
+  Var _ -> pure <$> f e
+  Cycle body -> liftA2 (:) (f e) (foreachSubterm f body)
+  Abs _ body -> liftA2 (:) (f e) (foreachSubterm f body)
+  Tm body -> liftA2 (:) (f e) (join . Foldable.toList <$> (sequenceA $ foreachSubterm f <$> body))
+
 -- | `visit f t` applies an effectful function to each subtree of
 -- `t` and sequences the results. When `f` returns `Nothing`, `visit`
 -- descends into the children of the current subtree. When `f` returns

parser-typechecker/src/Unison/Term.hs

@@ -185,10 +185,10 @@ derived = ref . Reference.Derived
 derived' :: Ord v => Text -> Maybe (Term' vt v)
 derived' base58 = derived <$> Hash.fromBase58 base58
 
-ref :: Ord v => Reference -> Term' vt v
+ref :: Ord v => Reference -> ABT.Term (F vt at) v ()
 ref r = ABT.tm (Ref r)
 
-builtin :: Ord v => Text -> Term' vt v
+builtin :: Ord v => Text -> ABT.Term (F vt at) v ()
 builtin n = ref (Reference.Builtin n)
 
 float :: Ord v => Double -> Term' vt v
@@ -236,6 +236,9 @@ iff cond t f = ABT.tm (If cond t f)
 ann :: Ord v => Term' vt v -> Type vt -> Term' vt v
 ann e t = ABT.tm (Ann e t)
 
+ann' :: Ord v => a -> ABT.Term (F vt at) v a -> Type.AnnotatedType vt at -> ABT.Term (F vt at) v a
+ann' a e t = ABT.tm' a (Ann e t)
+
 vector :: Ord v => [Term' vt v] -> Term' vt v
 vector es = ABT.tm (Vector (Vector.fromList es))
 

parser-typechecker/src/Unison/Typechecker/Context2.hs

@@ -89,6 +89,7 @@ data Note v loc
   | WithinSynthesizeApp (Type v loc) (Term v loc) (Note v loc)
   | TypeMismatch (Context v loc)
   | IllFormedType (Context v loc)
+  | UnknownSymbol loc v
   | CompilerBug (CompilerBug v loc)
   | AbilityCheckFailure [Type v loc] [Type v loc] -- ambient, requested
 
@@ -332,6 +333,14 @@ orElse m1 m2 = M go where
     r @ (_, Just (_, _)) -> r
     _ -> runM m2 menv
 
+-- If the action fails, preserve all the notes it emitted and then return the
+-- provided `a`; if the action succeeds, we're good, just use its result
+recover :: a -> M v loc a -> M v loc a
+recover ifFail (M action) = M go where
+  go menv = case action menv of
+    (notes, Nothing) -> (notes, Just (ifFail, env menv))
+    r -> r
+
 getDataDeclarations :: M v loc (DataDeclarations v loc)
 getDataDeclarations = M $ fromMEnv dataDecls
 
@@ -519,22 +528,21 @@ synthesize e = withinSynthesize e $ go (minimize' e)
   go (Term.Vector' v) = do
     ft <- vectorConstructorOfArity (Foldable.length v)
     foldM synthesizeApp ft v
-  -- go (Term.Let1' binding e) | Set.null (ABT.freeVars binding) = do
-  --   -- special case when it is definitely safe to generalize - binding contains
-  --   -- no free variables, i.e. `let id x = x in ...`
-  --   decls <- getDataDeclarations
-  --   abilities <- getAbilities
-  --   t  <- scope "let1 closed" $ synthesizeClosed' abilities decls binding
+  go (Term.Let1' binding e) | Set.null (ABT.freeVars binding) = do
+    -- special case when it is definitely safe to generalize - binding contains
+    -- no free variables, i.e. `let id x = x in ...`
+    abilities <- getAbilities
+    t  <- synthesizeClosed' abilities binding
+    v' <- ABT.freshen e freshenVar
+    e  <- pure $ ABT.bindInheritAnnotation e (Term.ann' () (Term.builtin (Var.name v')) t)
+    synthesize e
+  --go (Term.Let1' binding e) = do
+  --  -- literally just convert to a lambda application and call synthesize!
+  --  -- NB: this misses out on let generalization
+  --  -- let x = blah p q in foo y <=> (x -> foo y) (blah p q)
   --  v' <- ABT.freshen e freshenVar
-  --   e  <- pure $ ABT.bind e (Term.builtin (Var.name v') `Term.ann` t)
-  --   synthesize e
-  -- --go (Term.Let1' binding e) = do
-  -- --  -- literally just convert to a lambda application and call synthesize!
-  -- --  -- NB: this misses out on let generalization
-  -- --  -- let x = blah p q in foo y <=> (x -> foo y) (blah p q)
-  -- --  v' <- ABT.freshen e freshenVar
-  -- --  e  <- pure $ ABT.bind e (Term.var v')
-  -- --  synthesize (Term.lam v' e `Term.app` binding)
+  --  e  <- pure $ ABT.bind e (Term.var v')
+  --  synthesize (Term.lam v' e `Term.app` binding)
   -- go (Term.Let1' binding e) = do
   --   -- note: no need to freshen binding, it can't refer to v
   --   tbinding <- synthesize binding
@@ -915,6 +923,25 @@ abilityCheck requested = do
     ambient <- getAbilities
     abilityCheck' ambient requested
 
+verifyDataDeclarations :: (Eq loc, Var v) => DataDeclarations v loc -> M v loc ()
+verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do
+  let ctors = DD.constructors decl
+  forM_ ctors $ \(_ctorName,typ) ->
+    let isBoundIn v t = Set.member v (snd (ABT.annotation t))
+        loc t = fst (ABT.annotation t)
+        go t@(ABT.Var' v) | not (isBoundIn v t) = recover () $ failNote (UnknownSymbol (loc t) v)
+        go _ = pure ()
+    in ABT.foreachSubterm go (ABT.annotateBound typ)
+
+synthesizeClosed' :: (Eq loc, Var v)
+                  => [Type v loc]
+                  -> Term v loc
+                  -> M v loc (Type v loc)
+synthesizeClosed' abilities term = do
+  t <- withEffects0 abilities (synthesize term)
+  ctx <- getContext
+  pure $ generalizeExistentials ctx t
+
 instance (Var v, Show loc) => Show (Element v loc) where
   show (Var v) = case v of
     TypeVar.Universal x -> "@" <> show x