fixed versions of typeAt and admissibleTypeAt

src/Unison/Edit/Term.hs

@@ -8,7 +8,6 @@ import Unison.Edit.Term.Eval as Eval
 import qualified Unison.Syntax.Hash as H
 import qualified Unison.Note as N
 import Unison.Note (Noted)
-import qualified Unison.Syntax.Var
 import qualified Unison.Syntax.Term as E
 import qualified Unison.Syntax.Type as T
 import Unison.Type (synthesize)
@@ -45,13 +44,38 @@ beta eval loc ctx = case P.at' loc ctx of
   Nothing -> N.failure $ invalid loc ctx
   Just (sub,replace) -> replace <$> step eval sub
 
+-- | Compute the type of the given subterm, unconstrained as much
+-- as possible by any local usages of that subterm. For example, in
+-- @\g -> map g [1,2,3]@, @g@ will have a type of @forall r . Int -> r@,
+-- and @map@ will have a type of @forall a b . (a -> b) -> [a] -> [b]@.
+typeAt :: Applicative f
+       => (H.Hash -> Noted f T.Type)
+       -> P.Path
+       -> E.Term
+       -> Noted f T.Type
+typeAt synthLit (P.Path []) ctx = synthesize synthLit ctx
+typeAt synthLit loc ctx = case P.at' loc ctx of
+  Nothing -> N.failure $ invalid loc ctx
+  Just (sub,replace) ->
+    let ctx = E.lam1 $ \f -> replace (ksub f)
+        -- we annotate `f` as returning `Number` so as not to introduce
+        -- any new quantified variables in the inferred type
+        -- copy the subtree so type is unconstrained by local usage
+        ksub f = E.lam2 (\x _ -> x) `E.App` sub `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number)
+        go (T.Arrow (T.Arrow tsub _) _) = tsub
+        go (T.Forall n t) = T.Forall n (go t)
+        go _ = error "impossible, f had better be a function"
+    in go <$> synthesize synthLit ctx
+
 -- | Compute the allowed type of a replacement for a given subterm.
 -- Example, in @\g -> map g [1,2,3]@, @g@ has an admissible type of
 -- @forall r . Int -> r@, which means that an @Int -> Bool@, an
 -- @Int -> String@, etc could all be substituted for @g@.
 --
 -- Algorithm works by replacing the subterm, @e@ with
--- @const e (f e)@, where @f@ is a fresh function parameter. We then
+-- @const e (f e)@, where @f@ is a fresh function parameter and
+-- @e@ is let once in an outer scope, ensuring type information
+-- flows between the usage of @e@ and the call to @f@. We then
 -- read off the type of @e@ from the inferred type of @f@.
 admissibleTypeAt :: Applicative f
                  => (H.Hash -> Noted f T.Type)
@@ -62,29 +86,15 @@ admissibleTypeAt synthLit (P.Path []) ctx = synthesize synthLit ctx
 admissibleTypeAt synthLit loc ctx = case P.at' loc ctx of
   Nothing -> N.failure $ invalid loc ctx
   Just (sub,replace) ->
-    let ctx = E.lam1 $ \f -> replace (ksub f)
+    let ctx = (E.lam2 $ \sub f -> replace (ksub sub f)) `E.App` sub
         -- we annotate `f` as returning `Number` so as not to introduce
         -- any new quantified variables in the inferred type
-        ksub f = E.lam2 (\x y -> x) `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number)
+        ksub sub f = E.lam2 (\x _ -> x) `E.App` sub `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number)
         go (T.Arrow (T.Arrow tsub _) _) = tsub
         go (T.Forall n t) = T.Forall n (go t)
+        go _ = error "impossible, f had better be a function"
     in go <$> synthesize synthLit ctx
 
--- | Compute the type of the given subterm, unconstrained as much
--- as possible by any local usages of that subterm. For example, in
--- @\g -> map g [1,2,3]@, @g@ will have a type of @forall r . Int -> r@,
--- and @map@ will have a type of @forall a b . (a -> b) -> [a] -> [b]@.
-typeAt :: (Monad f, Applicative f)
-       => (H.Hash -> Noted f T.Type)
-       -> P.Path
-       -> E.Term
-       -> Noted f T.Type
-typeAt synthLit (P.Path []) ctx = synthesize synthLit ctx
-typeAt synthLit loc ctx = case P.at loc ctx of
-  Nothing -> N.failure $ invalid loc ctx
-  Just sub -> letFloat loc ctx >>= \(ctx,loc) ->
-    admissibleTypeAt synthLit loc ctx
-
 -- | Extract the given subterm into a let (implemented with a lambda)
 -- floated out as far as possible while ensuring access to all the
 -- variables used by the subterm. Examples: