Merge pull request #26 from unisonweb/topic/annotated-symbols

Make `Term` and `Type` agnostic to the type of variables, in prep for supporting rich function layou

node/default.nix

@@ -17,7 +17,7 @@ mkDerivation {
     transformers-compat unison-shared vector
   ];
   testDepends = [
-    base tasty tasty-hunit tasty-quickcheck tasty-smallcheck
+    base bytes tasty tasty-hunit tasty-quickcheck tasty-smallcheck
     unison-shared
   ];
   homepage = "http://unisonweb.org";

node/src/Node.hs

@@ -1,17 +1,19 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module Main where
 
-import Control.Applicative
 import Data.Text (Text)
-import Unison.Eval (Eval)
-import Unison.Hash (Hash)
+import Data.Bytes.Serial (Serial)
 import Unison.Metadata (Metadata(..))
 import Unison.Node (Node)
 import Unison.Node.Store (Store)
 import Unison.Term (Term)
 import Unison.Type (Type)
+import Unison.Var (Var)
+import Unison.Symbol.Extra ()
 import qualified Data.Map as M
 import qualified Data.Vector as Vector
 import qualified Unison.Eval as Eval
@@ -26,12 +28,13 @@ import qualified Unison.Reference as R
 import qualified Unison.Symbol as Symbol
 import qualified Unison.Term as Term
 import qualified Unison.Type as Type
+import qualified Unison.Var as Var
 
 infixr 7 -->
-(-->) :: Type -> Type -> Type
+(-->) :: Ord v => Type v -> Type v -> Type v
 (-->) = Type.arrow
 
-makeNode :: Store IO -> IO (Node IO R.Reference Type Term)
+makeNode :: forall v . (Serial v, Var v) => Store IO v -> IO (Node IO v R.Reference (Type v) (Term v))
 makeNode store =
   let
     builtins =
@@ -153,16 +156,9 @@ makeNode store =
        in (r, strict r 1, Type.forall' ["a"] $ view (v' "a") --> v' "a" --> v' "a", prefix "view")
      ]
 
-    eval :: Eval (N.Noted IO)
     eval = I.eval (M.fromList [ (k,v) | (k,Just v,_,_) <- builtins ])
-
-    readTerm :: Hash -> N.Noted IO Term
     readTerm h = Store.readTerm store h
-
-    whnf :: Term -> N.Noted IO Term
     whnf = Eval.whnf eval readTerm
-
-    node :: Node IO R.Reference Type Term
     node = C.node eval store
 
     v' = Type.v'
@@ -187,14 +183,14 @@ makeNode store =
                      where reapply args' = Term.ref r `apps` args' `apps` drop n args
             apps f args = foldl Term.app f args
 
-    numeric2 :: Term -> (Double -> Double -> Double) -> I.Primop (N.Noted IO)
+    numeric2 :: Term v -> (Double -> Double -> Double) -> I.Primop (N.Noted IO) v
     numeric2 sym f = I.Primop 2 $ \xs -> case xs of
       [x,y] -> g <$> whnf x <*> whnf y
         where g (Term.Number' x) (Term.Number' y) = Term.lit (Term.Number (f x y))
               g x y = sym `Term.app` x `Term.app` y
       _ -> error "unpossible"
 
-    string2 :: Term -> (Text -> Text -> Text) -> I.Primop (N.Noted IO)
+    string2 :: Term v -> (Text -> Text -> Text) -> I.Primop (N.Noted IO) v
     string2 sym f = I.Primop 2 $ \xs -> case xs of
       [x,y] -> g <$> whnf x <*> whnf y
         where g (Term.Text' x) (Term.Text' y) = Term.lit (Term.Text (f x y))
@@ -207,23 +203,20 @@ makeNode store =
           builtins
     pure node
 
-opl :: Int -> Text -> Metadata k
-opl n s = Metadata Metadata.Term
-                   (Metadata.Names [Symbol.symbol s Symbol.InfixL n ])
-                   []
-                   Nothing
+opl :: Var v => Int -> Text -> Metadata v h
+opl prec s = Metadata Metadata.Term
+                      (Metadata.Names [Var.named s])
+                      Nothing
 
-prefix :: Text -> Metadata k
+prefix :: Var v => Text -> Metadata v h
 prefix s = prefixes [s]
 
-prefixes :: [Text] -> Metadata k
+prefixes :: Var v => [Text] -> Metadata v h
 prefixes s = Metadata Metadata.Term
-                    (Metadata.Names (map (\s -> Symbol.symbol s Symbol.Prefix 9) s))
-                    []
-                    Nothing
-
+                      (Metadata.Names (map Var.named s))
+                      Nothing
 main :: IO ()
 main = do
-  store <- Store.store "store"
+  store <- Store.store "store" :: IO (Store IO (Symbol.Symbol (Maybe ())))
   node <- makeNode store
   S.server 8080 node

node/src/Unison/ABT/Extra.hs

@@ -12,7 +12,7 @@ import Data.Ord
 import Data.Vector ((!))
 import Prelude hiding (abs,cycle)
 import Unison.ABT
-import Unison.Symbol.Extra () -- `Serial` instances
+import Unison.Var (Var)
 import qualified Data.Bytes.Get as Get
 import qualified Data.Bytes.Put as Put
 import qualified Data.Set as Set
@@ -20,12 +20,13 @@ import qualified Data.Foldable as Foldable
 import qualified Data.Map as Map
 import qualified Data.Vector as Vector
 import qualified Unison.Digest as Digest
+import qualified Unison.Var as Var
 
 -- | We ignore annotations in the `Term`, as these should never affect the
 -- meaning of the term.
-hash :: forall f a . (Foldable f, Digest.Digestable1 f) => Term f a -> Digest.Hash
+hash :: forall f v a . (Foldable f, Digest.Digestable1 f, Var v) => Term f v a -> Digest.Hash
 hash t = hash' [] t where
-  hash' :: [Either [V] V] -> Term f a -> Digest.Hash
+  hash' :: [Either [v] v] -> Term f v a -> Digest.Hash
   hash' env (Term _ _ t) = case t of
     Var v -> maybe die hashInt ind
       where lookup (Left cycle) = elem v cycle
@@ -34,13 +35,13 @@ hash t = hash' [] t where
             -- env not likely to be very big, prefer to encode in one byte if possible
             hashInt :: Int -> Digest.Hash
             hashInt i = Digest.run (serialize (VarInt i))
-            die = error $ "unknown var in environment: " ++ show v
+            die = error $ "unknown var in environment: " ++ show (Var.name v)
     Cycle (AbsN' vs t) -> hash' (Left vs : env) t
     Cycle t -> hash' env t
     Abs v t -> hash' (Right v : env) t
     Tm t -> Digest.digest1 (hashCycle env) (hash' env) $ t
 
-  hashCycle :: [Either [V] V] -> [Term f a] -> Digest.DigestM (Term f a -> Digest.Hash)
+  hashCycle :: [Either [v] v] -> [Term f v a] -> Digest.DigestM (Term f v a -> Digest.Hash)
   hashCycle env@(Left cycle : envTl) ts | length cycle == length ts =
     let
       permute p xs = case Vector.fromList xs of xs -> map (xs !) p
@@ -53,17 +54,17 @@ hash t = hash' [] t where
   hashCycle env ts = Foldable.traverse_ (serialize . hash' env) ts *> pure (hash' env)
 
 -- | Use the `hash` function to efficiently remove duplicates from the list, preserving order.
-distinct :: (Foldable f, Digest.Digestable1 f) => [Term f a] -> [Term f a]
+distinct :: (Foldable f, Digest.Digestable1 f, Var v) => [Term f v a] -> [Term f v a]
 distinct ts = map fst (sortBy (comparing snd) m)
   where m = Map.elems (Map.fromList (map hash ts `zip` (ts `zip` [0 :: Int .. 1])))
 
 -- | Use the `hash` function to remove elements from `t1s` that exist in `t2s`, preserving order.
-subtract :: (Foldable f, Digest.Digestable1 f) => [Term f a] -> [Term f a] -> [Term f a]
+subtract :: (Foldable f, Digest.Digestable1 f, Var v) => [Term f v a] -> [Term f v a] -> [Term f v a]
 subtract t1s t2s =
   let skips = Set.fromList (map hash t2s)
   in filter (\t -> Set.notMember (hash t) skips) t1s
 
-instance (Foldable f, Serial a, Serial1 f) => Serial (Term f a) where
+instance (Foldable f, Serial a, Serial v, Ord v, Serial1 f) => Serial (Term f v a) where
   serialize (Term _ a e) = serialize a *> case e of
     Var v -> Put.putWord8 0 *> serialize v
     Cycle body -> Put.putWord8 1 *> serialize body

node/src/Unison/Eval/Interpreter.hs

@@ -6,25 +6,26 @@ import Data.Map (Map)
 import Debug.Trace
 import Unison.Eval
 import Unison.Term (Term)
+import Unison.Var (Var)
 import qualified Data.Map as M
 import qualified Unison.Reference as R
 import qualified Unison.Term as E
 
 -- | A Haskell function accepting 'arity' arguments
-data Primop f =
-  Primop { arity :: Int, call :: [Term] -> f Term }
+data Primop f v =
+  Primop { arity :: Int, call :: [Term v] -> f (Term v) }
 
 watch :: Show a => String -> a -> a
 watch msg a = trace (msg ++ ": " ++ show a) a
 
 -- | Produce an evaluator from a environment of 'Primop' values
-eval :: (Applicative f, Monad f) => Map R.Reference (Primop f) -> Eval f
+eval :: (Applicative f, Monad f, Var v) => Map R.Reference (Primop f v) -> Eval f v
 eval env = Eval whnf step
   where
-    reduce x args | trace ("reduce:" ++ show (x:args)) False = undefined
+    -- reduce x args | trace ("reduce:" ++ show (x:args)) False = undefined
     reduce (E.Lam' _ _) [] = return Nothing
     reduce e@(E.Lam' _ _) (arg1:args) =
-      return $ let r = watch "reduced" $ E.betaReduce (E.app e arg1)
+      return $ let r = E.betaReduce (E.app e arg1)
                in Just (foldl E.app r args)
     reduce (E.Ref' h) args = case M.lookup h env of
       Nothing -> return Nothing

node/src/Unison/Hash/Extra.hs

@@ -1,7 +1,6 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Unison.Hash.Extra where
 
-import Control.Applicative
 import Data.Bytes.Serial
 import Unison.Hash
 

node/src/Unison/Node.hs

@@ -17,31 +17,37 @@ import qualified Unison.Metadata as Metadata
 -- that previously returned incomplete results. Appending characters to a
 -- search that returned complete results just filters down the set and
 -- can be done client-side, assuming the client has the full result set.
-data SearchResults k t e =
+data SearchResults v h t e =
   SearchResults
     { query :: Metadata.Query
-    , references :: [(k, Metadata k)]
+    , references :: [(h, Metadata v h)]
     , matches :: ([e], Int)
     , illTypedMatches :: ([e], Int)
     , positionsExamined :: [Int] }
 
 deriveJSON defaultOptions ''SearchResults
 
-data Node m k t e = Node {
+-- | The Unison Node API:
+--   * `m` is the monad
+--   * `v` is the type of variables
+--   * `h` is the type of hashes
+--   * `t` is for type
+--   * `e` is for term (pnemonic "expression")
+data Node m v h t e = Node {
   -- | Obtain the type of the given subterm, assuming the path is valid
   admissibleTypeAt :: e -> Term.Path -> Noted m t,
   -- | Create a new term and provide its metadata
-  createTerm :: e -> Metadata k -> Noted m k,
+  createTerm :: e -> Metadata v h -> Noted m h,
   -- | Create a new type and provide its metadata
-  createType :: t -> Metadata k -> Noted m k,
+  createType :: t -> Metadata v h -> Noted m h,
   -- | Lookup the direct dependencies of @k@, optionally limited to the given set
-  dependencies :: Maybe (Set k) -> k -> Noted m (Set k),
+  dependencies :: Maybe (Set h) -> h -> Noted m (Set h),
   -- | Lookup the set of terms/types depending directly on the given @k@, optionally limited to the given set
-  dependents :: Maybe (Set k) -> k -> Noted m (Set k),
+  dependents :: Maybe (Set h) -> h -> Noted m (Set h),
   -- | Modify the given subterm, which may fail. First argument is the root path.
   -- Second argument is path relative to the root.
   -- Returns (root path, original e, edited e, new cursor position)
-  editTerm :: Term.Path -> Term.Path -> Action -> e -> Noted m (Maybe (Term.Path,e,e,Term.Path)),
+  editTerm :: Term.Path -> Term.Path -> Action v -> e -> Noted m (Maybe (Term.Path,e,e,Term.Path)),
   -- Evaluate all terms, returning a list of (path, original e, evaluated e)
   evaluateTerms :: [(Term.Path, e)] -> Noted m [(Term.Path,e,e)],
   -- | Returns ( subterm at the given path
@@ -53,22 +59,19 @@ data Node m k t e = Node {
   -- | Modify the given subterm, which may fail. First argument is the root path.
   localInfo :: e -> Term.Path -> Noted m (e, t, t, [e], [Int], [e]),
   -- | Access the metadata for the term and/or types identified by @k@
-  metadatas :: [k] -> Noted m (Map k (Metadata k)),
+  metadatas :: [h] -> Noted m (Map h (Metadata v h)),
   -- | Search for a term, optionally constrained to be of the given type
-  search :: e -> Term.Path -> Int -> Metadata.Query -> Maybe t -> Noted m (SearchResults k t e),
-  -- | Lookup the source of the term identified by @k@
-  terms :: [k] -> Noted m (Map k e),
-  -- | Lookup the dependencies of @k@, optionally limited to those that intersect the given set
-  transitiveDependencies :: Maybe (Set k) -> k -> Noted m (Set k),
+  search :: e -> Term.Path -> Int -> Metadata.Query -> Maybe t -> Noted m (SearchResults v h t e),
+  -- | Lookup the source of the term identified by @h@
+  terms :: [h] -> Noted m (Map h e),
+  -- | Lookup the dependencies of @h@, optionally limited to those that intersect the given set
+  transitiveDependencies :: Maybe (Set h) -> h -> Noted m (Set h),
   -- | Lookup the set of terms or types which depend on the given @k@, optionally limited to those that intersect the given set
-  transitiveDependents :: Maybe (Set k) -> k -> Noted m (Set k),
-  -- | Lookup the source of the type identified by @k@
-  types :: [k] -> Noted m (Map k t),
+  transitiveDependents :: Maybe (Set h) -> h -> Noted m (Set h),
+  -- | Lookup the source of the type identified by @h@
+  types :: [h] -> Noted m (Map h t),
   -- | Obtain the type of the given subterm, assuming the path is valid
   typeAt :: e -> Term.Path -> Noted m t,
   -- | Update the metadata associated with the given term or type
-  updateMetadata :: k -> Metadata k -> Noted m ()
+  updateMetadata :: h -> Metadata v h -> Noted m ()
 }
-
-
-

node/src/Unison/Node/Implementation.hs

@@ -2,8 +2,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 module Unison.Node.Implementation (node) where
 
-import Control.Applicative
 import Control.Monad
+import Data.Bytes.Serial (Serial)
 import Data.List
 import Data.Ord
 import Unison.Eval as Eval
@@ -13,6 +13,7 @@ import Unison.Term.Extra ()
 import Unison.Type (Type)
 import Unison.Node.Store (Store)
 import Unison.Note (Noted)
+import Unison.Var (Var)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Unison.ABT.Extra as ABT'
@@ -36,7 +37,10 @@ import qualified Unison.Node.Store as Store
 --watches :: (Foldable f, Show a) => String -> f a -> f a
 --watches msg as = trace (msg ++ ":\n" ++ intercalate "\n" (map show (Foldable.toList as)) ++ "\n.") as
 
-node :: (Applicative f, Monad f) => Eval (Noted f) -> Store f -> Node f Reference.Reference Type Term
+node :: (Monad f, Var v, Serial v)
+     => Eval (Noted f) v
+     -> Store f v
+     -> Node f v Reference.Reference (Type v) (Term v)
 node eval store =
   let
     readTypeOf = Store.typeOfTerm store
@@ -160,4 +164,3 @@ node eval store =
        types
        typeAt
        updateMetadata
-

node/src/Unison/Node/Store.hs

@@ -22,18 +22,20 @@ import qualified Unison.Hash as Hash
 import qualified Unison.Note as Note
 import qualified Unison.Reference as Reference
 
-data Store f = Store {
+-- todo may want to just bind v here
+
+data Store f v = Store {
   hashes :: Maybe (Set Reference) -> Noted f (Set Reference), -- ^ The set of hashes in this store, optionally constrained to intersect the given set
-  readTerm :: Hash -> Noted f Term,
-  writeTerm :: Hash -> Term -> Noted f (),
-  typeOfTerm :: Reference -> Noted f Type,
-  annotateTerm :: Reference -> Type -> Noted f (),
-  readMetadata :: Reference -> Noted f (Metadata Reference),
-  writeMetadata :: Reference -> Metadata Reference -> Noted f ()
+  readTerm :: Hash -> Noted f (Term v),
+  writeTerm :: Hash -> Term v -> Noted f (),
+  typeOfTerm :: Reference -> Noted f (Type v),
+  annotateTerm :: Reference -> Type v -> Noted f (),
+  readMetadata :: Reference -> Noted f (Metadata v Reference),
+  writeMetadata :: Reference -> Metadata v Reference -> Noted f ()
 }
 
 -- | Create a 'Store' rooted at the given path.
-store :: FilePath -> IO (Store IO)
+store :: (Ord v, ToJSON v, FromJSON v) => FilePath -> IO (Store IO v)
 store root =
   let
     hashesIn :: (String -> Reference) -> FilePath -> Noted IO (Set Reference)

node/src/Unison/NodeServer.hs

@@ -5,11 +5,14 @@
 module Unison.NodeServer where
 
 import Control.Monad.IO.Class
+import Data.Aeson (ToJSON, FromJSON)
 import Network.HTTP.Types.Method (StdMethod(OPTIONS))
 import Unison.Hash (Hash)
 import Unison.Node (Node)
 import Unison.Note (Noted, unnote)
 import Unison.Reference (Reference)
+import Unison.Term (Term)
+import Unison.Type (Type)
 import Web.Scotty (ActionM)
 import qualified Data.Aeson as J
 import qualified Data.Aeson.Parser as JP
@@ -58,7 +61,7 @@ route action = do
 postRoute :: S.RoutePattern -> ActionM () -> S.ScottyM ()
 postRoute s action = S.post s (route action)
 
-server :: Int -> Node IO Reference T.Type E.Term -> IO ()
+server :: (Ord v, ToJSON v, FromJSON v) => Int -> Node IO v Reference (Type v) (Term v) -> IO ()
 server port node = S.scotty port $ do
   S.addroute OPTIONS (S.regex ".*") $ originOptions
   postRoute "/admissible-type-at" $ do

node/src/Unison/Symbol/Extra.hs

@@ -1,21 +1,13 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Unison.Symbol.Extra where
 
-import Control.Applicative
 import Unison.Symbol
 import Data.Bytes.Serial (Serial(..))
 import Data.Bytes.VarInt
 
-instance Serial Fixity where
-  serialize = serialize . VarInt . fromEnum
-  deserialize = toEnum . unVarInt <$> deserialize
-
-instance Serial Symbol where
-  serialize (Symbol i n f p) =
-    serialize (VarInt i) *> serialize n *> serialize f *> serialize (VarInt p)
+instance Serial a => Serial (Symbol a) where
+  serialize (Symbol i n a) =
+    serialize (VarInt i) *> serialize n *> serialize a
   deserialize =
-    Symbol <$> (unVarInt <$> deserialize)
-           <*> deserialize
-           <*> deserialize
-           <*> (unVarInt <$> deserialize)
+    Symbol <$> (unVarInt <$> deserialize) <*> deserialize <*> deserialize
 

node/src/Unison/Term/Extra.hs

@@ -17,7 +17,7 @@ import qualified Unison.Hash as Hash
 import qualified Unison.Reference as Reference
 
 instance Serial Literal
-instance Serial1 F where
+instance (Serial v, Ord v) => Serial1 (F v) where
   serializeWith f e = case e of
     Lit l -> Put.putWord8 0 *> serialize l
     Blank -> Put.putWord8 1
@@ -44,7 +44,7 @@ instance Serial1 Vector where
   serializeWith f vs = serialize (Vector.length vs) *> traverse_ f vs
   deserializeWith v = deserialize >>= \len -> sequence (Vector.replicate len v)
 
-instance Digest.Digestable1 F where
+instance (Serial v, Ord v) => Digest.Digestable1 (F v) where
   digest1 hashCycle hash e = case e of
     -- References are 'transparent' wrt hash - we return the precomputed hash,
     -- so for example `x = 1 + 1` and `y = x` hash the same. Thus hashing is

node/src/Unison/TermEdit/Extra.hs

@@ -6,4 +6,4 @@ import Data.Bytes.Serial
 import Unison.Symbol.Extra ()
 import Unison.TermEdit
 
-instance Serial Action
+instance Serial v => Serial (Action v)

node/tests/Unison/Test/Term.hs

@@ -4,17 +4,23 @@ module Unison.Test.Term where
 import Unison.Term
 import Unison.Term.Extra ()
 import Unison.Reference as R
+import Unison.Var (Var)
+import Unison.Symbol (Symbol)
+import Unison.Symbol.Extra ()
 import Test.Tasty
 -- import Test.Tasty.SmallCheck as SC
 -- import Test.Tasty.QuickCheck as QC
 import Test.Tasty.HUnit
 import qualified Unison.ABT.Extra as ABT
 
+-- term for testing
+type TTerm = Term (Symbol (Maybe ()))
+
 tests :: TestTree
 tests = testGroup "Term"
   [ testCase "alpha equivalence (term)" $ assertEqual "identity"
-     (lam' ["a"] $ var' "a")
-     (lam' ["x"] $ var' "x")
+     ((lam' ["a"] $ var' "a") :: TTerm)
+      (lam' ["x"] $ var' "x")
   , testCase "hash cycles" $ assertEqual "pingpong"
      (ABT.hash pingpong1)
      (ABT.hash pingpong2)
@@ -22,37 +28,37 @@ tests = testGroup "Term"
 
 -- various unison terms, useful for testing
 
-id :: Term
+id :: TTerm
 id = lam' ["a"] $ var' "a"
 
-const :: Term
+const :: TTerm
 const = lam' ["x", "y"] $ var' "x"
 
-one :: Term
+one :: TTerm
 one = num 1
 
-zero :: Term
+zero :: TTerm
 zero = num 0
 
-plus :: Term -> Term -> Term
+plus :: TTerm -> TTerm -> TTerm
 plus a b = ref (R.Builtin "+") `app` a `app` b
 
-minus :: Term -> Term -> Term
+minus :: TTerm -> TTerm -> TTerm
 minus a b = ref (R.Builtin "-") `app` a `app` b
 
-fix :: Term
+fix :: TTerm
 fix = letRec'
   [ ("fix", lam' ["f"] $ var' "f" `app` (var' "fix" `app` var' "f")) ]
   (var' "fix")
 
-pingpong1 :: Term
+pingpong1 :: TTerm
 pingpong1 =
   letRec'
     [ ("ping", lam' ["x"] $ var' "pong" `app` (plus (var' "x") one))
     , ("pong", lam' ["y"] $ var' "pong" `app` (minus (var' "y") one)) ]
     (var' "ping" `app` one)
 
-pingpong2 :: Term
+pingpong2 :: TTerm
 pingpong2 =
   letRec'
     [ ("pong1", lam' ["p"] $ var' "pong1" `app` (minus (var' "p") one))

node/tests/Unison/Test/Typechecker.hs

@@ -8,6 +8,8 @@ import Unison.Term as E
 import Unison.Type as T
 import Unison.Typechecker as Typechecker
 import Unison.Reference as R
+import Unison.Symbol (Symbol)
+import Unison.Symbol.Extra ()
 import qualified Unison.Test.Term as Term
 
 import Test.Tasty
@@ -15,15 +17,19 @@ import Test.Tasty
 -- import Test.Tasty.QuickCheck as QC
 import Test.Tasty.HUnit
 
+type TTerm = Term.TTerm
+type TType = Type (Symbol (Maybe ()))
+type TEnv f = T.Env f (Symbol (Maybe ()))
+
 infixr 1 -->
-(-->) :: Type -> Type -> Type
+(-->) :: TType -> TType -> TType
 (-->) = T.arrow
 
-data StrongEq = StrongEq Type
+data StrongEq = StrongEq TType
 instance Eq StrongEq where StrongEq t1 == StrongEq t2 = Typechecker.equals t1 t2
 instance Show StrongEq where show (StrongEq t) = show t
 
-synthesizes :: Term -> Type -> Assertion
+synthesizes :: TTerm -> TType -> Assertion
 synthesizes e t =
   let
     handle r = case r of
@@ -31,23 +37,23 @@ synthesizes e t =
       Right _ -> pure ()
   in
     handle $ do
-      t2 <- (run (Typechecker.synthesize env e)) :: Either Note Type
+      t2 <- (run (Typechecker.synthesize env e)) :: Either Note TType
       _ <- Typechecker.subtype t2 t
       _ <- Typechecker.subtype t t2
       pure ()
 
-checks :: Term -> Type -> Assertion
+checks :: TTerm -> TType -> Assertion
 checks e t =
-  case (run (Typechecker.check env e t)) :: Either Note Type of
+  case (run (Typechecker.check env e t)) :: Either Note TType of
     Left err -> assertFailure ("checking failure: " ++ show err)
     Right t2 -> pure ()
 
-checkSubtype :: Type -> Type -> Assertion
+checkSubtype :: TType -> TType -> Assertion
 checkSubtype t1 t2 = case Typechecker.subtype t1 t2 of
   Left err -> assertFailure ("subtype failure:\n" ++ show err)
   Right t2 -> pure ()
 
-synthesizesAndChecks :: Term -> Type -> Assertion
+synthesizesAndChecks :: TTerm -> TType -> Assertion
 synthesizesAndChecks e t =
   synthesizes e t >> checks e t
 
@@ -91,7 +97,7 @@ tests = testGroup "Typechecker"
       (forall' ["a"] $ T.v' "a")
   ]
 
-env :: Applicative f => T.Env f
+env :: Applicative f => TEnv f
 env r =
   let
     view a = T.app (T.ref (R.Builtin "View")) a

node/unison-node.cabal

@@ -136,6 +136,7 @@ test-suite tests
   else
     build-depends:
       base,
+      bytes,
       tasty,
       tasty-hunit,
       tasty-smallcheck,

shared/src/Unison/ABT.hs

@@ -1,10 +1,11 @@
 -- Based on: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module Unison.ABT where
@@ -17,40 +18,39 @@ import Data.Text (Text)
 import Data.Traversable
 import Prelude hiding (abs,cycle)
 import Prelude.Extras (Eq1(..), Show1(..))
-import Unison.Symbol (Symbol)
+import Unison.Var (Var)
 import qualified Data.Aeson as Aeson
 import qualified Data.Foldable as Foldable
 import qualified Data.Set as Set
 import qualified Data.Text as Text
 import qualified Unison.JSON as J
-import qualified Unison.Symbol as Symbol
+import qualified Unison.Var as Var
 
-type V = Symbol
-
-data ABT f r
-  = Var V
+data ABT f v r
+  = Var v
   | Cycle r
-  | Abs V r
+  | Abs v r
   | Tm (f r) deriving (Functor, Foldable, Traversable)
 
 -- | At each level in the tree, we store the set of free variables and
--- a value of type `a`.
-data Term f a = Term { freeVars :: Set V, annotation :: a, out :: ABT f (Term f a) }
+-- a value of type `a`. Individual variables are annotated with a value of
+-- type `v`.
+data Term f v a = Term { freeVars :: Set v, annotation :: a, out :: ABT f v (Term f v a) }
 
 -- | `True` if the term has no free variables, `False` otherwise
-isClosed :: Term f a -> Bool
+isClosed :: Term f v a -> Bool
 isClosed t = Set.null (freeVars t)
 
 -- | `True` if `v` is a member of the set of free variables of `t`
-isFreeIn :: V -> Term f a -> Bool
+isFreeIn :: Ord v => v -> Term f v a -> Bool
 isFreeIn v t = Set.member v (freeVars t)
 
 -- | Replace the annotation with the given argument.
-annotate :: a -> Term f a -> Term f a
+annotate :: a -> Term f v a -> Term f v a
 annotate a (Term fvs _ out) = Term fvs a out
 
 -- | Modifies the annotations in this tree
-instance Functor f => Functor (Term f) where
+instance Functor f => Functor (Term f v) where
   fmap f (Term fvs a sub) = Term fvs (f a) (fmap (fmap f) sub)
 
 pattern Var' v <- Term _ _ (Var v)
@@ -59,41 +59,41 @@ pattern Abs' v body <- Term _ _ (Abs v body)
 pattern AbsN' vs body <- (unabs -> (vs, body))
 pattern Tm' f <- Term _ _ (Tm f)
 
-v' :: Text -> V
-v' = Symbol.prefix
+v' :: Var v => Text -> v
+v' = Var.named
 
-var :: V -> Term f ()
+var :: v -> Term f v ()
 var = annotatedVar ()
 
-var' :: Text -> Term f ()
-var' v = var (Symbol.prefix v)
+var' :: Var v => Text -> Term f v ()
+var' v = var (Var.named v)
 
-annotatedVar :: a -> V -> Term f a
+annotatedVar :: a -> v -> Term f v a
 annotatedVar a v = Term (Set.singleton v) a (Var v)
 
-abs :: V -> Term f () -> Term f ()
+abs :: Ord v => v -> Term f v () -> Term f v ()
 abs = abs' ()
 
-abs' :: a -> V -> Term f a -> Term f a
+abs' :: Ord v => a -> v -> Term f v a -> Term f v a
 abs' a v body = Term (Set.delete v (freeVars body)) a (Abs v body)
 
-tm :: Foldable f => f (Term f ()) -> Term f ()
+tm :: (Foldable f, Ord v) => f (Term f v ()) -> Term f v ()
 tm = tm' ()
 
-tm' :: Foldable f => a -> f (Term f a) -> Term f a
+tm' :: (Foldable f, Ord v) => a -> f (Term f v a) -> Term f v a
 tm' a t =
   Term (Set.unions (fmap freeVars (Foldable.toList t))) a (Tm t)
 
-cycle :: Term f () -> Term f ()
+cycle :: Term f v () -> Term f v ()
 cycle = cycle' ()
 
-cycle' :: a -> Term f a -> Term f a
+cycle' :: a -> Term f v a -> Term f v a
 cycle' a t = Term (freeVars t) a (Cycle t)
 
-into :: Foldable f => ABT f (Term f ()) -> Term f ()
+into :: (Foldable f, Ord v) => ABT f v (Term f v ()) -> Term f v ()
 into = into' ()
 
-into' :: Foldable f => a -> ABT f (Term f a) -> Term f a
+into' :: (Foldable f, Ord v) => a -> ABT f v (Term f v a) -> Term f v a
 into' a abt = case abt of
   Var x -> annotatedVar a x
   Cycle t -> cycle' a t
@@ -101,7 +101,7 @@ into' a abt = case abt of
   Tm t -> tm' a t
 
 -- | renames `old` to `new` in the given term, ignoring subtrees that bind `old`
-rename :: (Foldable f, Functor f) => V -> V -> Term f a -> Term f a
+rename :: (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a
 rename old new t0@(Term _ ann t) = case t of
   Var v -> if v == old then annotatedVar ann new else t0
   Cycle body -> cycle' ann (rename old new body)
@@ -110,46 +110,43 @@ rename old new t0@(Term _ ann t) = case t of
   Tm v -> tm' ann (fmap (rename old new) v)
 
 -- | Produce a variable which is free in both terms
-freshInBoth :: Term f a -> Term f a -> V -> V
+freshInBoth :: Var v => Term f v a -> Term f v a -> v -> v
 freshInBoth t1 t2 = fresh t2 . fresh t1
 
-fresh :: Term f a -> V -> V
+fresh :: Var v => Term f v a -> v -> v
 fresh t = fresh' (freeVars t)
 
-fresh' :: Set V -> V -> V
-fresh' used = Symbol.freshIn used
+fresh' :: Var v => Set v -> v -> v
+fresh' used = Var.freshIn used
 
-freshes :: Term f a -> [V] -> [V]
-freshes t = freshes' (freeVars t)
+freshes :: Var v => Term f v a -> [v] -> [v]
+freshes t = Var.freshes (freeVars t)
 
-freshes' :: Set V -> [V] -> [V]
-freshes' _ [] = []
-freshes' used (h:t) =
-  let h' = fresh' used h
-  in h' : freshes' (Set.insert h' used) t
+freshes' :: Var v => Set v -> [v] -> [v]
+freshes' = Var.freshes
 
-freshNamed' :: Set V -> Text -> V
+freshNamed' :: Var v => Set v -> Text -> v
 freshNamed' used n = fresh' used (v' n)
 
 -- | `subst t x body` substitutes `t` for `x` in `body`, avoiding capture
-subst :: (Foldable f, Functor f) => Term f a -> V -> Term f a -> Term f a
+subst :: (Foldable f, Functor f, Var v) => Term f v a -> v -> Term f v a -> Term f v a
 subst t x body = replace t match body where
   match (Var' v) = x == v
   match _ = False
 
 -- | `substs [(t1,v1), (t2,v2), ...] body` performs multiple simultaneous
 -- substitutions, avoiding capture
-substs :: (Foldable f, Functor f) => [(V, Term f a)] -> Term f a -> Term f a
+substs :: (Foldable f, Functor f, Var v) => [(v, Term f v a)] -> Term f v a -> Term f v a
 substs replacements body = foldr f body replacements where
   f (v, t) body = subst t v body
 
 -- | `replace t f body` substitutes `t` for all maximal (outermost)
 -- subterms matching the predicate `f` in `body`, avoiding capture.
-replace :: (Foldable f, Functor f)
-        => Term f a
-        -> (Term f a -> Bool)
-        -> Term f a
-        -> Term f a
+replace :: (Foldable f, Functor f, Var v)
+        => Term f v a
+        -> (Term f v a -> Bool)
+        -> Term f v a
+        -> Term f v a
 replace t f body | f body = t
 replace t f t2@(Term _ ann body) = case body of
   Var v -> annotatedVar ann v
@@ -167,7 +164,10 @@ replace t f t2@(Term _ ann body) = case body of
 -- `Just t2`, `visit` replaces the current subtree with `t2`. Thus:
 -- `visit (const Nothing) t == pure t` and
 -- `visit (const (Just (pure t2))) t == pure t2`
-visit :: (Traversable f, Applicative g) => (Term f () -> Maybe (g (Term f ()))) -> Term f () -> g (Term f ())
+visit :: (Traversable f, Applicative g, Ord v)
+      => (Term f v () -> Maybe (g (Term f v ())))
+      -> Term f v ()
+      -> g (Term f v ())
 visit f t = case f t of
   Just gt -> gt
   Nothing -> case out t of
@@ -177,8 +177,10 @@ visit f t = case f t of
     Tm body -> tm <$> traverse (visit f) body
 
 -- | Apply an effectful function to an ABT tree top down, sequencing the results.
-visit' :: (Traversable f, Applicative g, Monad g)
-       => (f (Term f ()) -> g (f (Term f ()))) -> Term f () -> g (Term f ())
+visit' :: (Traversable f, Applicative g, Monad g, Ord v)
+       => (f (Term f v ()) -> g (f (Term f v ())))
+       -> Term f v ()
+       -> g (Term f v ())
 visit' f t = case out t of
   Var _ -> pure t
   Cycle body -> cycle <$> visit' f body
@@ -190,22 +192,22 @@ visit' f t = case out t of
 type Focus1 f a = f a -> Maybe (a, a -> f a)
 
 -- | Extract the subterm at a given path
-at :: Foldable f => [Focus1 f (Term f a)] ->  Term f a -> Maybe (Term f a)
+at :: (Foldable f, Ord v) => [Focus1 f (Term f v a)] -> Term f v a -> Maybe (Term f v a)
 at path t = fst <$> focus path t
 
 -- | Modify the subterm a path points to
-modify :: Foldable f
-       => (Term f a -> Term f a)
-       -> [Focus1 f (Term f a)]
-       -> Term f a
-       -> Maybe (Term f a)
+modify :: (Foldable f, Ord v)
+       => (Term f v a -> Term f v a)
+       -> [Focus1 f (Term f v a)]
+       -> Term f v a
+       -> Maybe (Term f v a)
 modify f path t = (\(t,replace) -> replace (f t)) <$> focus path t
 
 -- | Focus on a subterm, obtaining the subtree and a function to replace that subtree
-focus :: Foldable f
-      => [Focus1 f (Term f a)]
-      -> Term f a
-      -> Maybe (Term f a, Term f a -> Term f a)
+focus :: (Foldable f, Ord v)
+      => [Focus1 f (Term f v a)]
+      -> Term f v a
+      -> Maybe (Term f v a, Term f v a -> Term f v a)
 focus [] t = Just (t, id)
 focus path@(hd:tl) (Term _ ann t) = case t of
   Var _ -> Nothing
@@ -222,25 +224,25 @@ focus path@(hd:tl) (Term _ ann t) = case t of
 
 -- | Returns the longest prefix of the path which points to a subterm
 -- in which `v` is not bound.
-introducedAt :: V -> [Focus1 f (Term f ())] -> Term f () -> Maybe [Focus1 f (Term f ())]
+introducedAt :: Ord v => v -> [Focus1 f (Term f v ())] -> Term f v () -> Maybe [Focus1 f (Term f v ())]
 introducedAt v path t = f =<< boundAlong path t where
   f bs = case dropWhile (\vs -> not (Set.member v vs)) (reverse bs) of
     [] -> if elem v (fst (unabs t)) then Just [] else Nothing
     p -> Just (take (length p) path)
 
 -- | Returns the set of variables in scope at the given path, if valid
-boundAt :: [Focus1 f (Term f ())] -> Term f () -> Maybe (Set V)
+boundAt :: Ord v => [Focus1 f (Term f v ())] -> Term f v () -> Maybe (Set v)
 boundAt path t = f =<< boundAlong path t where
   f [] = Nothing
   f vs = Just (last vs)
 
 -- | Returns the set of variables in scope at the given path,
 -- or the empty set if path is invalid
-boundAt' :: [Focus1 f (Term f ())] -> Term f () -> Set V
+boundAt' :: Ord v => [Focus1 f (Term f v ())] -> Term f v () -> Set v
 boundAt' path t = fromMaybe Set.empty (boundAt path t)
 
 -- | For each element of the input path, the set of variables in scope
-boundAlong :: [Focus1 f (Term f ())] -> Term f () -> Maybe [Set V]
+boundAlong :: Ord v => [Focus1 f (Term f v ())] -> Term f v () -> Maybe [Set v]
 boundAlong path t = go Set.empty path t where
   go _ [] _ = Just []
   go env path@(hd:tl) t = case out t of
@@ -252,15 +254,15 @@ boundAlong path t = go Set.empty path t where
       tl <- go env tl t
       pure (env : tl)
 
-unabs :: Term f a -> ([V], Term f a)
+unabs :: Term f v a -> ([v], Term f v a)
 unabs (Term _ _ (Abs hd body)) =
   let (tl, body') = unabs body in (hd : tl, body')
 unabs t = ([], t)
 
-reabs :: [V] -> Term f () -> Term f ()
+reabs :: Ord v => [v] -> Term f v () -> Term f v ()
 reabs vs t = foldr abs t vs
 
-instance (Foldable f, Functor f, Eq1 f, Eq a) => Eq (Term f a) where
+instance (Foldable f, Functor f, Eq1 f, Eq a, Var v) => Eq (Term f v a) where
   -- alpha equivalence, works by renaming any aligned Abs ctors to use a common fresh variable
   t1 == t2 = annotation t1 == annotation t2 && go (out t1) (out t2) where
     go (Var v) (Var v2) | v == v2 = True
@@ -272,7 +274,7 @@ instance (Foldable f, Functor f, Eq1 f, Eq a) => Eq (Term f a) where
     go (Tm f1) (Tm f2) = f1 ==# f2
     go _ _ = False
 
-instance (J.ToJSON1 f, ToJSON a) => ToJSON (Term f a) where
+instance (J.ToJSON1 f, ToJSON v, ToJSON a) => ToJSON (Term f v a) where
   toJSON (Term _ a e) =
     let
       body = case e of
@@ -283,7 +285,7 @@ instance (J.ToJSON1 f, ToJSON a) => ToJSON (Term f a) where
     in
       J.array [toJSON a, body]
 
-instance (Foldable f, J.FromJSON1 f, FromJSON a) => FromJSON (Term f a) where
+instance (Foldable f, J.FromJSON1 f, FromJSON v, Ord v, FromJSON a) => FromJSON (Term f v a) where
   parseJSON j = do
     ann <- J.at 0 Aeson.parseJSON j
     J.at 1 (\j -> do {
@@ -296,10 +298,10 @@ instance (Foldable f, J.FromJSON1 f, FromJSON a) => FromJSON (Term f a) where
         _                -> fail ("unknown tag: " ++ Text.unpack t)
     }) j
 
-instance Show1 f => Show (Term f a) where
+instance (Show1 f, Var v) => Show (Term f v a) where
   -- annotations not shown
   showsPrec p (Term _ _ out) = case out of
-    Var v -> showsPrec 0 v
+    Var v -> showsPrec 0 (Var.shortName v)
     Cycle body -> showsPrec p body
-    Abs v body -> showParen True $ showsPrec 0 v . showString ". " . showsPrec p body
+    Abs v body -> showParen True $ showsPrec 0 (Var.shortName v) . showString ". " . showsPrec p body
     Tm f -> showsPrec1 p f

shared/src/Unison/Eval.hs

@@ -3,7 +3,7 @@ module Unison.Eval where
 import Unison.Hash (Hash)
 import Unison.Term (Term)
 
-data Eval m = Eval {
-  whnf :: (Hash -> m Term) -> Term -> m Term, -- ^ Simplify to weak head normal form
-  step :: (Hash -> m Term) -> Term -> m Term  -- ^ Perform one beta reduction
+data Eval m v = Eval {
+  whnf :: (Hash -> m (Term v)) -> Term v -> m (Term v), -- ^ Simplify to weak head normal form
+  step :: (Hash -> m (Term v)) -> Term v -> m (Term v)  -- ^ Perform one beta reduction
 }

shared/src/Unison/Metadata.hs

@@ -4,34 +4,32 @@ module Unison.Metadata where
 import Data.Aeson
 import Data.Aeson.TH
 import Data.Text (Text)
-import Unison.Symbol (Symbol)
+import Unison.Var (Var)
 import qualified Data.Text as Text
-import qualified Unison.Symbol as Symbol
-import qualified Unison.Term as Term
+import qualified Unison.Var as Var
 
 data Sort = Type | Term deriving (Eq,Ord,Show)
 
-data Metadata k =
+data Metadata v h =
   Metadata {
     sort :: Sort,
-    names :: Names,
-    locals :: [(Term.Path, Symbol)],
-    description :: Maybe k
+    names :: Names v,
+    description :: Maybe h
   } deriving (Eq,Ord,Show)
 
-matches :: Query -> Metadata k -> Bool
-matches (Query txt) (Metadata _ (Names ns) _ _) =
-  any (Text.isPrefixOf txt) (map Symbol.name ns)
+matches :: Var v => Query -> Metadata v h -> Bool
+matches (Query txt) (Metadata _ (Names ns) _) =
+  any (Text.isPrefixOf txt) (map Var.name ns)
 
 -- | Nameless metadata, contains only the annotation
-synthetic :: Sort -> Metadata k
-synthetic t = Metadata t (Names []) [] Nothing
+synthetic :: Sort -> Metadata v h
+synthetic t = Metadata t (Names []) Nothing
 
 -- | Nameless term metadata, containing only the type annotation
-syntheticTerm :: Metadata k
+syntheticTerm :: Metadata v h
 syntheticTerm = synthetic Term
 
-data Names = Names [Symbol] deriving (Eq,Ord,Show)
+data Names v = Names [v] deriving (Eq,Ord,Show)
 
 data Query = Query Text
 

shared/src/Unison/Symbol.hs

@@ -1,35 +1,49 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleInstances #-}
 module Unison.Symbol where
 
 import Data.Aeson.TH
 import Data.Text (Text)
-import Data.Set (Set)
+import Unison.Var (Var(..))
 import qualified Data.Set as Set
 import qualified Data.Text as Text
 
-data Fixity = InfixL | InfixR | Infix | Prefix deriving (Eq,Ord,Show,Enum)
-
 -- NB: freshId is first field, so given a `Set Symbol`, the max element of
 -- the set will also have the highest `freshId`.
-data Symbol = Symbol { freshId :: !Int, name :: Text, fixity :: !Fixity, precedence :: !Int } deriving (Eq,Ord)
+data Symbol a = Symbol !Int Text a
 
-instance Show Symbol where
+freshId :: Symbol a -> Int
+freshId (Symbol id _ _) = id
+
+annotation :: Symbol a -> a
+annotation (Symbol _ _ a) = a
+
+instance Var (Symbol (Maybe a)) where
+  name (Symbol _ n _) = n
+  named n = Symbol 0 n Nothing
+  qualifiedName s = name s `Text.append` (Text.pack (show (freshId s)))
+  freshIn vs s | Set.null vs = s -- already fresh!
+  freshIn vs s | Set.notMember s vs = s -- already fresh!
+  freshIn vs s@(Symbol i n a) = case Set.elemAt (Set.size vs - 1) vs of
+    Symbol i2 _ _ -> if i > i2 then s else Symbol (i2+1) n a
+
+instance Functor Symbol where
+  fmap f (Symbol id name a) = Symbol id name (f a)
+
+-- Note: The `annotation` field not part of identity, is "just" metadata
+instance Eq (Symbol a) where
+  Symbol id1 name1 _ == Symbol id2 name2 _ = id1 == id2 && name1 == name2
+instance Ord (Symbol a) where
+  Symbol id1 name1 _ `compare` Symbol id2 name2 _ = (id1,name1) `compare` (id2,name2)
+
+instance Show (Symbol (Maybe a)) where
   show s | freshId s == 0 = Text.unpack (name s)
   show s = Text.unpack (name s) ++ show (freshId s)
 
-symbol :: Text -> Fixity -> Int -> Symbol
-symbol n f p = Symbol 0 n f p
+symbol :: Text -> Symbol ()
+symbol n = Symbol 0 n ()
 
--- | Returns a fresh version of the given symbol, guaranteed to
--- be distinct from all symbols in the given set. Takes time
--- logarithmic in the size of the symbol set.
-freshIn :: Set Symbol -> Symbol -> Symbol
-freshIn vs s | Set.notMember s vs = s -- already fresh!
-freshIn vs s@(Symbol i n f p) = case Set.elemAt (Set.size vs - 1) vs of
-  Symbol i2 _ _ _ -> if i > i2 then s else Symbol (i2+1) n f p
+prefix :: Text -> Symbol ()
+prefix name = symbol name
 
-prefix :: Text -> Symbol
-prefix name = symbol name Prefix 9
-
-deriveJSON defaultOptions ''Fixity
 deriveJSON defaultOptions ''Symbol

shared/src/Unison/Term.hs

@@ -13,6 +13,7 @@ module Unison.Term where
 import Control.Applicative
 import Control.Monad
 import Data.Aeson.TH
+import Data.Aeson (ToJSON, FromJSON)
 import Data.List
 import Data.Maybe
 import Data.Set (Set)
@@ -23,6 +24,8 @@ import Prelude.Extras (Eq1(..), Show1(..))
 import Text.Show
 import Unison.Hash (Hash)
 import Unison.Reference (Reference)
+import Unison.Type (Type)
+import Unison.Var (Var)
 import qualified Control.Monad.Writer.Strict as Writer
 import qualified Data.Aeson as Aeson
 import qualified Data.Monoid as Monoid
@@ -30,7 +33,6 @@ import qualified Data.Set as Set
 import qualified Data.Vector as Vector
 import qualified Unison.ABT as ABT
 import qualified Unison.Reference as Reference
-import qualified Unison.Type as T
 import qualified Unison.Distance as Distance
 import qualified Unison.JSON as J
 
@@ -42,12 +44,12 @@ data Literal
   deriving (Eq,Ord,Generic)
 
 -- | Base functor for terms in the Unison language
-data F a
+data F v a
   = Lit Literal
   | Blank -- An expression that has not been filled in, has type `forall a . a`
   | Ref Reference
   | App a a
-  | Ann a T.Type
+  | Ann a (Type v)
   | Vector (Vector a)
   | Lam a
   -- Invariant: let rec blocks have an outer ABT.Cycle which introduces as many
@@ -56,10 +58,12 @@ data F a
   | Let a a
   deriving (Eq,Foldable,Functor,Generic1,Traversable)
 
--- | Terms are represented as ABTs over the base functor F.
-type AnnotatedTerm a = ABT.Term F a
+-- | Like `Term v`, but with an annotation of type `a` at every level in the tree
+type AnnotatedTerm v a = ABT.Term (F v) v a
+
+-- | Terms are represented as ABTs over the base functor F, with variables in `v`
+type Term v = AnnotatedTerm v ()
 
-type Term = AnnotatedTerm ()
 -- nicer pattern syntax
 
 pattern Var' v <- ABT.Var' v
@@ -76,90 +80,90 @@ pattern Let1' v b e <- (ABT.out -> ABT.Tm (Let b (ABT.Abs' v e)))
 pattern Let' bs e relet rec <- (unLets -> Just (bs,e,relet,rec))
 pattern LetRec' bs e <- (unLetRec -> Just (bs,e))
 
-fresh :: Term -> ABT.V -> ABT.V
+fresh :: Var v => Term v -> v -> v
 fresh = ABT.fresh
 
 -- some smart constructors
 
-var :: ABT.V -> Term
+var :: v -> Term v
 var = ABT.var
 
-var' :: Text -> Term
+var' :: Var v => Text -> Term v
 var' = var . ABT.v'
 
-ref :: Reference -> Term
+ref :: Ord v => Reference -> Term v
 ref r = ABT.tm (Ref r)
 
-num :: Double -> Term
+num :: Ord v => Double -> Term v
 num = lit . Number
 
-lit :: Literal -> Term
+lit :: Ord v => Literal -> Term v
 lit l = ABT.tm (Lit l)
 
-blank :: Term
+blank :: Ord v => Term v
 blank = ABT.tm Blank
 
-app :: Term -> Term -> Term
+app :: Ord v => Term v -> Term v -> Term v
 app f arg = ABT.tm (App f arg)
 
-apps :: Term -> [Term] -> Term
+apps :: Ord v => Term v -> [Term v] -> Term v
 apps f = foldl' app f
 
-ann :: Term -> T.Type -> Term
+ann :: Ord v => Term v -> Type v -> Term v
 ann e t = ABT.tm (Ann e t)
 
-vector :: [Term] -> Term
+vector :: Ord v => [Term v] -> Term v
 vector es = ABT.tm (Vector (Vector.fromList es))
 
-vector' :: Vector Term -> Term
+vector' :: Ord v => Vector (Term v) -> Term v
 vector' es = ABT.tm (Vector es)
 
-lam :: ABT.V -> Term -> Term
+lam :: Ord v => v -> Term v -> Term v
 lam v body = ABT.tm (Lam (ABT.abs v body))
 
-lam' :: [Text] -> Term -> Term
+lam' :: Var v => [Text] -> Term v -> Term v
 lam' vs body = foldr lam body (map ABT.v' vs)
 
 -- | Smart constructor for let rec blocks. Each binding in the block may
 -- reference any other binding in the block in its body (including itself),
 -- and the output expression may also reference any binding in the block.
-letRec :: [(ABT.V,Term)] -> Term -> Term
+letRec :: Ord v => [(v,Term v)] -> Term v -> Term v
 letRec [] e = e
 letRec bindings e = ABT.cycle (foldr ABT.abs z (map fst bindings))
   where
     z = ABT.tm (LetRec (map snd bindings) e)
 
-letRec' :: [(Text, Term)] -> Term -> Term
+letRec' :: Var v => [(Text, Term v)] -> Term v -> Term v
 letRec' bs e = letRec [(ABT.v' name, b) | (name,b) <- bs] e
 
 -- | Smart constructor for let blocks. Each binding in the block may
 -- reference only previous bindings in the block, not including itself.
 -- The output expression may reference any binding in the block.
-let1 :: [(ABT.V,Term)] -> Term -> Term
+let1 :: Ord v => [(v,Term v)] -> Term v -> Term v
 let1 bindings e = foldr f e bindings
   where
     f (v,b) body = ABT.tm (Let b (ABT.abs v body))
 
-let1' :: [(Text,Term)] -> Term -> Term
+let1' :: Var v => [(Text,Term v)] -> Term v -> Term v
 let1' bs e = let1 [(ABT.v' name, b) | (name,b) <- bs ] e
 
 -- | Satisfies
 --   `unLets (letRec bs e) == Just (bs, e, letRec, True)` and
 --   `unLets (let' bs e) == Just (bs, e, let', False)`
 -- Useful for writing code agnostic to whether a let block is recursive or not.
-unLets :: Term -> Maybe ([(ABT.V,Term)], Term, [(ABT.V,Term)] -> Term -> Term, Bool)
+unLets :: Ord v => Term v -> Maybe ([(v,Term v)], Term v, [(v,Term v)] -> Term v -> Term v, Bool)
 unLets e =
   (f letRec True <$> unLetRec e) <|> (f let1 False <$> unLet e)
   where f mkLet rec (bs,e) = (bs,e,mkLet,rec)
 
 -- | Satisfies `unLetRec (letRec bs e) == Just (bs, e)`
-unLetRec :: Term -> Maybe ([(ABT.V, Term)], Term)
+unLetRec :: Term v -> Maybe ([(v, Term v)], Term v)
 unLetRec (ABT.Cycle' vs (ABT.Tm' (LetRec bs e)))
   | length vs == length vs = Just (zip vs bs, e)
 unLetRec _ = Nothing
 
 -- | Satisfies `unLet (let' bs e) == Just (bs, e)`
-unLet :: Term -> Maybe ([(ABT.V, Term)], Term)
+unLet :: Term v -> Maybe ([(v, Term v)], Term v)
 unLet t = fixup (go t) where
   go (ABT.out -> ABT.Tm (Let b (ABT.Abs' v t))) =
     case go t of (env,t) -> ((v,b):env, t)
@@ -167,15 +171,15 @@ unLet t = fixup (go t) where
   fixup ([], _) = Nothing
   fixup bst = Just bst
 
-dependencies' :: Term -> Set Reference
+dependencies' :: Ord v => Term v -> Set Reference
 dependencies' t = Set.fromList . Writer.execWriter $ ABT.visit' f t
   where f t@(Ref r) = Writer.tell [r] *> pure t
         f t = pure t
 
-dependencies :: Term -> Set Hash
+dependencies :: Ord v => Term v -> Set Hash
 dependencies e = Set.fromList [ h | Reference.Derived h <- Set.toList (dependencies' e) ]
 
-countBlanks :: Term -> Int
+countBlanks :: Ord v => Term v -> Int
 countBlanks t = Monoid.getSum . Writer.execWriter $ ABT.visit' f t
   where f Blank = Writer.tell (Monoid.Sum (1 :: Int)) *> pure Blank
         f t = pure t
@@ -190,8 +194,8 @@ data PathElement
 
 type Path = [PathElement]
 
--- | Use a @PathElement@ to compute one step into an @F Term@ subexpression
-focus1 :: PathElement -> ABT.Focus1 F Term
+-- | Use a @PathElement@ to compute one step into an @F Term v@ subexpression
+focus1 :: Ord v => PathElement -> ABT.Focus1 (F v) (Term v)
 focus1 Fn (App f x) = Just (f, \f -> App f x)
 focus1 Arg (App f x) = Just (x, \x -> App f x)
 focus1 Body (Lam (ABT.Abs' v body)) = Just (body, Lam . ABT.abs v)
@@ -213,20 +217,20 @@ pathPrefixes = inits
 pathExtend :: PathElement -> Path -> Path
 pathExtend e p = p ++ [e]
 
-at :: Path -> Term -> Maybe Term
+at :: Ord v => Path -> Term v -> Maybe (Term v)
 at p t = ABT.at (map focus1 p) t
 
 -- | Given a variable and a path, find the longest prefix of the path
 -- which points to a term where the variable is unbound. Example:
 -- `\f -> \x -> f {x}` would return the path pointing to `{\x -> f x}`
-introducedAt :: ABT.V -> Path -> Term -> Maybe Path
+introducedAt :: Ord v => v -> Path -> Term v -> Maybe Path
 introducedAt v path t = f <$> ABT.introducedAt v (map focus1 path) t where
   f p = take (length p) path
 
-modify :: (Term -> Term) -> Path -> Term -> Maybe Term
+modify :: Ord v => (Term v -> Term v) -> Path -> Term v -> Maybe (Term v)
 modify f p t = ABT.modify f (map focus1 p) t
 
-focus :: Path -> Term -> Maybe (Term, Term -> Term)
+focus :: Ord v => Path -> Term v -> Maybe (Term v, Term v -> Term v)
 focus p t = ABT.focus (map focus1 p) t
 
 parent :: Path -> Maybe Path
@@ -236,7 +240,7 @@ parent p = Just (init p)
 parent' :: Path -> Path
 parent' = fromMaybe [] . parent
 
-bindingAt :: Path -> Term -> Maybe (ABT.V, Term)
+bindingAt :: Ord v => Path -> Term v -> Maybe (v, Term v)
 bindingAt [] _ = Nothing
 bindingAt path t = do
   parentPath <- parent path
@@ -244,7 +248,7 @@ bindingAt path t = do
   pure (v, b)
 
 -- | Convert all 'Ref' constructors to the corresponding term
-link :: (Applicative f, Monad f) => (Hash -> f Term) -> Term -> f Term
+link :: (Applicative f, Monad f, Var v) => (Hash -> f (Term v)) -> Term v -> f (Term v)
 link env e =
   let ds = map (\h -> (h, link env =<< env h)) (Set.toList (dependencies e))
       sub e (h, ft) = replace <$> ft
@@ -254,21 +258,23 @@ link env e =
 
 -- | If the outermost term is a function application,
 -- perform substitution of the argument into the body
-betaReduce :: Term -> Term
+betaReduce :: Var v => Term v -> Term v
 betaReduce (App' (Lam' n body) arg) = ABT.subst arg n body
 betaReduce e = e
 
--- mostly boring serialization and hashing code below ...
+-- mostly boring serialization code below ...
 
 deriveJSON defaultOptions ''Literal
 
-instance Eq1 F where (==#) = (==)
-instance Show1 F where showsPrec1 = showsPrec
+instance Var v => Eq1 (F v) where (==#) = (==)
+instance Var v => Show1 (F v) where showsPrec1 = showsPrec
 
-deriveJSON defaultOptions ''F
-instance J.ToJSON1 F where toJSON1 f = Aeson.toJSON f
-instance J.FromJSON1 F where parseJSON1 j = Aeson.parseJSON j
+deriveToJSON defaultOptions ''F
+instance (Ord v, FromJSON v, FromJSON r) => FromJSON (F v r) where
+  parseJSON = $(mkParseJSON defaultOptions ''F)
 
+instance ToJSON v => J.ToJSON1 (F v) where toJSON1 f = Aeson.toJSON f
+instance (Ord v, FromJSON v) => J.FromJSON1 (F v) where parseJSON1 j = Aeson.parseJSON j
 
 deriveJSON defaultOptions ''PathElement
 
@@ -277,7 +283,7 @@ instance Show Literal where
   show (Number n) = show n
   show (Distance d) = show d
 
-instance Show a => Show (F a) where
+instance (Var v, Show a) => Show (F v a) where
   showsPrec p fa = go p fa where
     go _ (Lit l) = showsPrec 0 l
     go p (Ann t k) = showParen (p > 1) $ showsPrec 0 t <> s":" <> showsPrec 0 k

shared/src/Unison/TermEdit.hs

@@ -14,13 +14,14 @@ import Unison.Hash (Hash)
 import Unison.Term (Term)
 import Unison.Type (Type)
 import Unison.Note (Noted)
+import Unison.Var (Var)
 import qualified Data.Set as Set
 import qualified Unison.ABT as ABT
 import qualified Unison.Eval as Eval
 import qualified Unison.Term as Term
 import qualified Unison.Type as Type
 
-data Action
+data Action v
   = Abstract -- Turn target into function parameter
   | AbstractLet -- Turn target into let bound expression
   | AllowRec -- Turn a let into a let rec
@@ -29,7 +30,7 @@ data Action
   | Inline -- Delete a let binding by inlining its definition into usage sites
   | MergeLet -- Merge a let block into its parent let block
   | Noop -- Do nothing to the target
-  | Rename ABT.V -- Rename the target var
+  | Rename v -- Rename the target var
   | Step -- Link + beta reduce the target
   | SwapDown -- Swap the target let binding with the subsequent binding
   | SwapUp -- Swap the target let binding with the previous binding
@@ -37,10 +38,10 @@ data Action
   deriving Generic
 
 -- | Interpret the given 'Action'
-interpret :: (Applicative f, Monad f)
-          => Eval (Noted f)
-          -> (Hash -> Noted f Term.Term)
-          -> Term.Path -> Action -> Term.Term -> Noted f (Maybe (Term.Path, Term.Term))
+interpret :: (Applicative f, Monad f, Var v)
+          => Eval (Noted f) v
+          -> (Hash -> Noted f (Term v))
+          -> Term.Path -> Action v -> Term v -> Noted f (Maybe (Term.Path, Term v))
 interpret eval link path action t = case action of
   Abstract -> pure $ abstract path t
   AbstractLet -> pure $ abstractLet path t
@@ -61,7 +62,7 @@ interpret eval link path action t = case action of
    ==>
    f {(v -> v) 42}
 -}
-abstract :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+abstract :: Var v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 abstract path t = f <$> Term.focus path t where
   f (sub,replace) =
     let sub' = Term.lam (ABT.fresh sub (ABT.v' "v")) (ABT.var' "v")
@@ -74,7 +75,7 @@ abstract path t = f <$> Term.focus path t where
    ==>
    f {let v = 42 in v} x
 -}
-abstractLet :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+abstractLet :: Var v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 abstractLet path t = f <$> Term.focus path t where
   f (sub,replace) =
     let sub' = Term.let1 [(ABT.v' "v", sub)] (ABT.var' "v")
@@ -85,7 +86,7 @@ abstractLet path t = f <$> Term.focus path t where
    ==>
    {let rec x = 1 in x + x}
 -}
-allowRec :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+allowRec :: Ord v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 allowRec path t = do
   Term.Let' bs e _ False <- Term.at path t
   t' <- Term.modify (const (Term.letRec bs e)) path t
@@ -96,13 +97,13 @@ allowRec path t = do
    ==>
    { f }
 -}
-etaReduce :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+etaReduce :: Ord v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 etaReduce path t = do
   Term.Lam' v (Term.App' f (ABT.Var' v2)) <- Term.at path t
   guard (v == v2 && not (Set.member v (ABT.freeVars f))) -- make sure vars match and `f` doesn't mention `v`
   pure (path, f)
 
-floatOut :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+floatOut :: Term.Path -> Term v -> Maybe (Term.Path, Term v)
 floatOut path t = floatLetOut path t <|> floatLamOut path t
 
 {- Moves the target let binding to the parent expression. Example:
@@ -110,7 +111,7 @@ floatOut path t = floatLetOut path t <|> floatLamOut path t
    ==>
    {let y = 2 in f (y*y)}
 -}
-floatLetOut :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+floatLetOut :: Term.Path -> Term v -> Maybe (Term.Path, Term v)
 floatLetOut _ _ =
   error "todo: floatLetOut"
 
@@ -119,7 +120,7 @@ floatLetOut _ _ =
    ==>
    {y -> f (y*y)} 2
 -}
-floatLamOut :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+floatLamOut :: Term.Path -> Term v -> Maybe (Term.Path, Term v)
 floatLamOut _ _ = error "floatLamOut"
 
 {- Delete a let binding by inlining its definition. Fails if binding is recursive. Examples:
@@ -135,7 +136,7 @@ floatLamOut _ _ = error "floatLamOut"
    ==>
    {let y = 2 in 1*1}
 -}
-inline :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+inline :: Ord v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 inline path t = do
   -- (v,body) <- Term.bindingAt path t
   (_,_) <- Term.bindingAt path t
@@ -150,7 +151,7 @@ inline path t = do
    in
      y*y}
 -}
-mergeLet :: Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+mergeLet :: Ord v => Term.Path -> Term v -> Maybe (Term.Path, Term v)
 mergeLet path t = do
   parentPath <- Term.parent path
   (innerBindings,e) <- Term.at path t >>= Term.unLetRec
@@ -161,22 +162,22 @@ mergeLet path t = do
     t
 
 {- Rename the variable at the target, updating all occurrences. -}
-rename :: ABT.V -> Term.Path -> Term.Term -> Maybe (Term.Path, Term.Term)
+rename :: Var v => v -> Term.Path -> Term v -> Maybe (Term.Path, Term v)
 rename v2 path t = do
   ABT.Var' v <- Term.at path t
   guard (v /= v2)
   scope <- Term.introducedAt v path t
   (,) scope <$> Term.modify (ABT.subst (ABT.var v2) v) scope t
 
-step :: Applicative f => Eval (Noted f) -> (Hash -> Noted f Term.Term)
-     -> Term.Path -> Term.Term -> Noted f (Maybe (Term.Path, Term.Term))
+step :: (Applicative f, Ord v) => Eval (Noted f) v -> (Hash -> Noted f (Term v))
+     -> Term.Path -> Term v -> Noted f (Maybe (Term.Path, Term v))
 step eval link path t = case Term.focus path t of
   Nothing -> pure Nothing
   Just (sub, replace) -> fmap f (Eval.step eval link sub)
     where f sub = Just (path, replace sub)
 
-whnf :: Applicative f => Eval (Noted f) -> (Hash -> Noted f Term.Term)
-     -> Term.Path -> Term.Term -> Noted f (Maybe (Term.Path, Term.Term))
+whnf :: (Applicative f, Ord v) => Eval (Noted f) v -> (Hash -> Noted f (Term v))
+     -> Term.Path -> Term v -> Noted f (Maybe (Term.Path, Term v))
 whnf eval link path t = case Term.focus path t of
   Nothing -> pure Nothing
   Just (sub, replace) -> fmap f (Eval.whnf eval link sub)
@@ -184,7 +185,7 @@ whnf eval link path t = case Term.focus path t of
 
 -- | Produce `e`, `e _`, `e _ _`, `e _ _ _` and so on,
 -- until the result is no longer a function type
-applications :: Term -> Type -> [Term]
+applications :: Ord v => Term v -> Type v -> [Term v]
 applications e t = e : go e t
   where
     go e (Type.Forall' _ t) = go e t

shared/src/Unison/Type.hs

@@ -10,7 +10,7 @@
 
 module Unison.Type where
 
-import Data.Aeson (toJSON, parseJSON)
+import Data.Aeson (ToJSON(..), FromJSON(..))
 import Data.Aeson.TH
 import Data.Set (Set)
 import Data.Text (Text)
@@ -18,12 +18,13 @@ import GHC.Generics
 import Prelude.Extras (Eq1(..),Show1(..))
 import Unison.Note (Noted)
 import Unison.Reference (Reference)
+import Unison.Var (Var)
 import qualified Data.Set as Set
 import qualified Unison.ABT as ABT
 import qualified Unison.Doc as D
 import qualified Unison.JSON as J
 import qualified Unison.Kind as K
-import qualified Unison.Symbol as Symbol
+import qualified Unison.Var as Var
 
 -- | Type literals
 data Literal
@@ -52,24 +53,25 @@ deriveJSON defaultOptions ''F
 instance Eq1 F where (==#) = (==)
 instance Show1 F where showsPrec1 = showsPrec
 
--- | Terms are represented as ABTs over the base functor F.
-type Type = ABT.Term F ()
+-- | Types are represented as ABTs over the base functor F, with variables in `v`
+type Type v = AnnotatedType v ()
 
-type AnnotatedType a = ABT.Term F a
+-- | Like `Type v`, but with an annotation of type `a` at every level in the tree
+type AnnotatedType v a = ABT.Term F v a
 
 -- An environment for looking up type references
-type Env f = Reference -> Noted f Type
+type Env f v = Reference -> Noted f (Type v)
 
-freeVars :: Type -> Set ABT.V
+freeVars :: Type v -> Set v
 freeVars = ABT.freeVars
 
-data Monotype = Monotype { getPolytype :: Type } deriving (Eq)
+data Monotype v = Monotype { getPolytype :: Type v } deriving (Eq)
 
-instance Show Monotype where
+instance Var v => Show (Monotype v) where
   show = show . getPolytype
 
 -- Smart constructor which checks if a `Type` has no `Forall` quantifiers.
-monotype :: Type -> Maybe Monotype
+monotype :: Ord v => Type v -> Maybe (Monotype v)
 monotype t = Monotype <$> ABT.visit isMono t where
   isMono (Forall' _ _) = Just Nothing
   isMono _ = Nothing
@@ -88,24 +90,24 @@ pattern Forall' v body <- ABT.Tm' (Forall (ABT.Abs' v body))
 pattern Existential' v <- ABT.Tm' (Existential (ABT.Var' v))
 pattern Universal' v <- ABT.Tm' (Universal (ABT.Var' v))
 
-unArrows :: Type -> Maybe [Type]
+unArrows :: Type v -> Maybe [Type v]
 unArrows t =
   case go t of [] -> Nothing; l -> Just l
   where
     go (Arrow' i o) = i : go o
     go _ = []
 
-unArrows' :: Type -> Maybe [(Type,Path)]
+unArrows' :: Type v -> Maybe [(Type v,Path)]
 unArrows' t = addPaths <$> unArrows t
   where addPaths ts = ts `zip` arrowPaths (length ts)
 
-unApps :: Type -> Maybe (Type, [Type])
+unApps :: Type v -> Maybe (Type v, [Type v])
 unApps t = case go t [] of [] -> Nothing; f:args -> Just (f,args)
   where
   go (App' i o) acc = go i (o:acc)
   go fn args = fn:args
 
-unApps' :: Type -> Maybe ((Type,Path), [(Type,Path)])
+unApps' :: Type v -> Maybe ((Type v,Path), [(Type v,Path)])
 unApps' t = addPaths <$> unApps t
   where
   addPaths (f,args) = case appPaths (length args) of
@@ -122,51 +124,51 @@ arrowPaths spineLength =
   (take (spineLength-1) $ iterate (Output:) [Input]) ++
   [replicate spineLength Output]
 
-matchExistential :: ABT.V -> Type -> Bool
+matchExistential :: Eq v => v -> Type v -> Bool
 matchExistential v (Existential' x) = x == v
 matchExistential _ _ = False
 
-matchUniversal :: ABT.V -> Type -> Bool
+matchUniversal :: Eq v => v -> Type v -> Bool
 matchUniversal v (Universal' x) = x == v
 matchUniversal _ _ = False
 
 -- some smart constructors
 
-lit :: Literal -> Type
+lit :: Ord v => Literal -> Type v
 lit l = ABT.tm (Lit l)
 
-ref :: Reference -> Type
+ref :: Ord v => Reference -> Type v
 ref = lit . Ref
 
-app :: Type -> Type -> Type
+app :: Ord v => Type v -> Type v -> Type v
 app f arg = ABT.tm (App f arg)
 
-arrow :: Type -> Type -> Type
+arrow :: Ord v => Type v -> Type v -> Type v
 arrow i o = ABT.tm (Arrow i o)
 
-ann :: Type -> K.Kind -> Type
+ann :: Ord v => Type v -> K.Kind -> Type v
 ann e t = ABT.tm (Ann e t)
 
-forall :: ABT.V -> Type -> Type
+forall :: Ord v => v -> Type v -> Type v
 forall v body = ABT.tm (Forall (ABT.abs v body))
 
-existential :: ABT.V -> Type
+existential :: Ord v => v -> Type v
 existential v = ABT.tm (Existential (ABT.var v))
 
-universal :: ABT.V -> Type
+universal :: Ord v => v -> Type v
 universal v = ABT.tm (Universal (ABT.var v))
 
-v' :: Text -> Type
+v' :: Var v => Text -> Type v
 v' s = universal (ABT.v' s)
 
-forall' :: [Text] -> Type -> Type
+forall' :: Var v => [Text] -> Type v -> Type v
 forall' vs body = foldr forall body (map ABT.v' vs)
 
-constrain :: Type -> () -> Type
+constrain :: Ord v => Type v -> () -> Type v
 constrain t u = ABT.tm (Constrain t u)
 
 -- | Bind all free variables with an outer `forall`.
-generalize :: Type -> Type
+generalize :: Ord v => Type v -> Type v
 generalize t = foldr forall t $ Set.toList (ABT.freeVars t)
 
 data PathElement
@@ -179,7 +181,7 @@ data PathElement
 
 type Path = [PathElement]
 
-layout :: (Reference -> ABT.V) -> Type -> D.Doc Text Path
+layout :: (Var v, ToJSON v) => (Reference -> v) -> Type v -> D.Doc Text Path
 layout ref t = go (0 :: Int) t
   where
   (<>) = D.append
@@ -188,13 +190,13 @@ layout ref t = go (0 :: Int) t
     Text -> "Text"
     Vector -> "Vector"
     Distance -> "Distance"
-    Ref r -> Symbol.name (ref r) -- no infix type operators at the moment
+    Ref r -> Var.name (ref r) -- no infix type operators at the moment
   paren b d =
     let r = D.root d
     in if b then D.embed' r "(" <> d <> D.embed' r ")" else d
   arr = D.breakable " " <> D.embed "→ "
   sp = D.breakable " "
-  sym v = D.embed (Symbol.name v)
+  sym v = D.embed (Var.name v)
   go p t = case t of
     Lit' l -> D.embed (lit l)
     ArrowsP' spine ->
@@ -206,12 +208,13 @@ layout ref t = go (0 :: Int) t
         , D.nest "  " . D.group . D.delimit sp $ [ D.sub' p (go 10 s) | (s,p) <- args ] ]
     Constrain' t _ -> go p t
     Universal' v -> sym v
-    Existential' v -> D.embed ("'" `mappend` Symbol.name v)
-    Ann' t k -> go p t -- ignoring kind annotations for now
+    Existential' v -> D.embed ("'" `mappend` Var.name v)
+    Ann' t _ -> go p t -- ignoring kind annotations for now
     Forall' v body -> case p of
       0 -> D.sub Body (go p body)
       _ -> paren True . D.group . D.docs $
              [D.embed "∀ ", sym v, D.embed ".", sp, D.nest "  " $ D.sub Body (go 0 body)]
+    _ -> error $ "layout match failure on: " ++ show (toJSON t)
 
 instance J.ToJSON1 F where
   toJSON1 f = toJSON f

shared/src/Unison/Typechecker.hs

@@ -8,6 +8,7 @@ import Control.Monad
 import Unison.Type (Type)
 import Unison.Term (Term)
 import Unison.Note (Note,Noted)
+import Unison.Var (Var)
 import qualified Unison.ABT as ABT
 import qualified Unison.Term as Term
 import qualified Unison.Type as Type
@@ -32,11 +33,11 @@ invalid loc ctx = "invalid path " ++ show loc ++ " in:\n" ++ show ctx
 --
 -- Note: the returned type may contain free type variables, since
 -- we strip off any outer foralls.
-admissibleTypeAt :: Applicative f
-                 => Type.Env f
+admissibleTypeAt :: (Applicative f, Var v)
+                 => Type.Env f v
                  -> Term.Path
-                 -> Term
-                 -> Noted f Type
+                 -> Term v
+                 -> Noted f (Type v)
 admissibleTypeAt synth loc t = Note.scoped ("admissibleTypeAt@" ++ show loc ++ " " ++ show t) $
   let
     f = Term.fresh t (ABT.v' "s")
@@ -48,7 +49,7 @@ admissibleTypeAt synth loc t = Note.scoped ("admissibleTypeAt@" ++ show loc ++ "
     Just t -> shake <$> synthesize synth t
 
 -- | Compute the type of the given subterm.
-typeAt :: Applicative f => Type.Env f -> Term.Path -> Term -> Noted f Type
+typeAt :: (Applicative f, Var v) => Type.Env f v -> Term.Path -> Term v -> Noted f (Type v)
 typeAt synth [] t = Note.scoped ("typeAt: " ++ show t) $ synthesize synth t
 typeAt synth loc t = Note.scoped ("typeAt@"++show loc ++ " " ++ show t) $
   let
@@ -61,12 +62,12 @@ typeAt synth loc t = Note.scoped ("typeAt@"++show loc ++ " " ++ show t) $
     Just t -> shake <$> synthesize synth t
 
 -- | Return the type of all local variables in scope at the given location
-locals :: Applicative f => Type.Env f -> Term.Path -> Term -> Noted f [(ABT.V, Type)]
+locals :: (Applicative f, Var v) => Type.Env f v -> Term.Path -> Term v -> Noted f [(v, Type v)]
 locals synth path ctx | ABT.isClosed ctx =
   Note.scoped ("locals@"++show path ++ " " ++ show ctx)
               (zip (map fst lambdas) <$> lambdaTypes)
   where
-    lambdas :: [(ABT.V, Term.Path)]
+    -- lambdas :: [(v, Term.Path)]
     lambdas = Term.pathPrefixes path >>= \path -> case Term.at path ctx of
       Just (Term.Lam' v _) -> [(v, path)]
       _ -> []
@@ -74,7 +75,7 @@ locals synth path ctx | ABT.isClosed ctx =
     lambdaTypes = traverse t (map snd lambdas)
       where t path = extract <$> typeAt synth path ctx
 
-    extract :: Type -> Type
+    extract :: Var v => Type v -> Type v
     extract (Type.Arrow' i _) = i
     extract (Type.Forall' _ t) = extract t
     extract t = error $ "expecting function type, got " ++ show t
@@ -84,12 +85,12 @@ locals _ _ ctx =
 -- | Infer the type of a 'Unison.Syntax.Term', using
 -- a function to resolve the type of @Ref@ constructors
 -- contained in that term.
-synthesize :: Applicative f => Type.Env f -> Term -> Noted f Type
+synthesize :: (Applicative f, Var v) => Type.Env f v -> Term v -> Noted f (Type v)
 synthesize = Context.synthesizeClosed
 
 -- | Infer the type of a 'Unison.Syntax.Term', assumed
 -- not to contain any @Ref@ constructors
-synthesize' :: Term -> Either Note Type
+synthesize' :: Var v => Term v -> Either Note (Type v)
 synthesize' term = join . Note.unnote $ synthesize missing term
   where missing h = Note.failure $ "unexpected ref: " ++ show h
 
@@ -97,18 +98,18 @@ synthesize' term = join . Note.unnote $ synthesize missing term
 -- function to resolve the type of @Ref@ constructors
 -- contained in the term. Returns @typ@ if successful,
 -- and a note about typechecking failure otherwise.
-check :: Applicative f => Type.Env f -> Term -> Type -> Noted f Type
+check :: (Applicative f, Var v) => Type.Env f v -> Term v -> Type v -> Noted f (Type v)
 check synth term typ = synthesize synth (Term.ann term typ)
 
 -- | Check whether a term, assumed to contain no @Ref@ constructors,
 -- matches a given type. Return @Left@ if any references exist, or
 -- if typechecking fails.
-check' :: Term -> Type -> Either Note Type
+check' :: Var v => Term v -> Type v -> Either Note (Type v)
 check' term typ = join . Note.unnote $ check missing term typ
   where missing h = Note.failure $ "unexpected ref: " ++ show h
 
 -- | Returns `True` if the expression is well-typed, `False` otherwise
-wellTyped :: (Monad f, Applicative f) => Type.Env f -> Term -> Noted f Bool
+wellTyped :: (Monad f, Var v) => Type.Env f v -> Term v -> Noted f Bool
 wellTyped synth term = (const True <$> synthesize synth term) `Note.orElse` pure False
 
 -- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
@@ -118,13 +119,13 @@ wellTyped synth term = (const True <$> synthesize synth term) `Note.orElse` pure
 -- about the reason for subtyping failure otherwise.
 --
 -- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
-subtype :: Type -> Type -> Either Note Type
+subtype :: Var v => Type v -> Type v -> Either Note (Type v)
 subtype t1 t2 = case Context.subtype (Context.context []) t1 t2 of
   Left e -> Left e
   Right _ -> Right t2
 
 -- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
-isSubtype :: Type -> Type -> Bool
+isSubtype :: Var v => Type v -> Type v -> Bool
 isSubtype t1 t2 = case Context.subtype (Context.context []) t1 t2 of
   Left _ -> False
   Right _ -> True
@@ -133,6 +134,6 @@ isSubtype t1 t2 = case Context.subtype (Context.context []) t1 t2 of
 -- order of quantifier introduction. Note that alpha equivalence considers:
 -- `forall b a . a -> b -> a` and
 -- `forall a b . a -> b -> a` to be different types
-equals :: Type -> Type -> Bool
+equals :: Var v => Type v -> Type v -> Bool
 equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1
 

shared/src/Unison/Typechecker/Context.hs

@@ -14,33 +14,36 @@ import Data.Set (Set)
 import Unison.Note (Note,Noted(..))
 import Unison.Term (Term)
 import Unison.Type (Type, Monotype(..))
-import qualified Unison.ABT as ABT
+import Unison.Var (Var)
 import qualified Data.Foldable as Foldable
-import qualified Unison.Note as Note
 import qualified Data.Set as Set
+import qualified Data.Text as Text
+import qualified Unison.ABT as ABT
+import qualified Unison.Note as Note
 import qualified Unison.Term as Term
 import qualified Unison.Type as Type
+import qualified Unison.Var as Var
 
 -- uncomment for debugging
 -- import Debug.Trace
 -- watch msg a = trace (msg ++ ":\n" ++ show a) a
 
 -- | Elements of an ordered algorithmic context
-data Element
-  = Universal ABT.V            -- `v` is universally quantified
-  | Existential ABT.V          -- `v` existential and unsolved
-  | Solved ABT.V Monotype      -- `v` is solved to some monotype
-  | Ann ABT.V Type             -- `v` has type `a`, which may be quantified
-  | Marker ABT.V deriving (Eq) -- used for scoping
+data Element v
+  = Universal v            -- `v` is universally quantified
+  | Existential v          -- `v` existential and unsolved
+  | Solved v (Monotype v)  -- `v` is solved to some monotype
+  | Ann v (Type v)         -- `v` has type `a`, which may be quantified
+  | Marker v deriving (Eq) -- used for scoping
 
-instance Show Element where
-  show (Universal v) = show v
-  show (Existential v) = "'"++show v
-  show (Solved v t) = "'"++show v++" = "++show t
-  show (Ann v t) = show v++" : "++show t
-  show (Marker v) = "|"++show v++"|"
+instance Var v => Show (Element v) where
+  show (Universal v) = Text.unpack (Var.shortName v)
+  show (Existential v) = "'"++Text.unpack (Var.shortName v)
+  show (Solved v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t
+  show (Ann v t) = Text.unpack (Var.shortName v)++" : "++show t
+  show (Marker v) = "|"++Text.unpack (Var.shortName v)++"|"
 
-(===) :: Element -> Element -> Bool
+(===) :: Eq v => Element v -> Element v -> Bool
 Existential v === Existential v2 | v == v2 = True
 Universal v   === Universal v2 | v == v2 = True
 Marker v      === Marker v2 | v == v2 = True
@@ -56,37 +59,36 @@ _ === _ = False
    is also a valid context, and a fresh name can be obtained just
    by inspecting the first `Info` in the list.
 -}
-newtype Context = Context [(Element, Info)]
+newtype Context v = Context [(Element v, Info v)]
 
-data Info = Info { existentialVars :: Set ABT.V -- set of existentials seen so far
-                 , universalVars :: Set ABT.V -- set of universals seen so far
-                 , allVars :: Set ABT.V -- all variables seen so far
-                 , isWellformed :: Bool -- whether the context so far is well-formed
-                 }
+data Info v =
+  Info { existentialVars :: Set v -- set of existentials seen so far
+       , universalVars :: Set v -- set of universals seen so far
+       , allVars :: Set v -- all variables seen so far
+       , isWellformed :: Bool -- whether the context so far is well-formed
+       }
 
 -- | The empty context
-context0 :: Context
+context0 :: Context v
 context0 = Context []
 
-instance Show Context where
-  show c@(Context es) =
-    "Γ " ++ show (Set.toList (usedVars c)) ++ "\n  "
-         ++ (intercalate "\n  " . map (show . fst)) (reverse es)
+instance Var v => Show (Context v) where
+  show (Context es) = "Γ \n" ++ (intercalate "\n  " . map (show . fst)) (reverse es)
 
 -- ctxOK :: Context -> Context
 -- ctxOK ctx = if wellformed ctx then ctx else error $ "not ok: " ++ show ctx
 
-usedVars :: Context -> Set ABT.V
+usedVars :: Context v -> Set v
 usedVars = allVars . info
 
 -- | Return the `Info` associated with the last element of the context, or the zero `Info`.
-info :: Context -> Info
+info :: Context v -> Info v
 info (Context []) = Info Set.empty Set.empty Set.empty True
 info (Context ((_,i):_)) = i
 
 -- | Add an element onto the end of this `Context`. Takes `O(log N)` time,
 -- including updates to the accumulated `Info` value.
-extend :: Element -> Context -> Context
+extend :: Var v => Element v -> Context v -> Context v
 extend e c@(Context ctx) = Context ((e,i'):ctx) where
   i' = addInfo e (info c)
   -- see figure 7
@@ -105,44 +107,44 @@ extend e c@(Context ctx) = Context ((e,i'):ctx) where
     Marker v -> Info es us (Set.insert v vs) (ok && Set.notMember v vs)
 
 -- | Build a context from a list of elements.
-context :: [Element] -> Context
+context :: Var v => [Element v] -> Context v
 context xs = foldl' (flip extend) context0 xs
 
 -- | `append c1 c2` adds the elements of `c2` onto the end of `c1`.
-append :: Context -> Context -> Context
+append :: Var v => Context v -> Context v -> Context v
 append ctxL (Context es) =
   -- since `es` is a snoc list, we add it to `ctxL` in reverse order
   foldl' f ctxL (reverse es) where
     f ctx (e,_) = extend e ctx
 
 -- Generate a fresh variable of the given name, guaranteed fresh wrt `ctx`.
-fresh :: ABT.V -> Context -> ABT.V
+fresh :: Var v => v -> Context v -> v
 fresh v ctx = ABT.fresh' (usedVars ctx) v
 
 -- Generate two fresh variables of the given names, guaranteed fresh wrt `ctx`.
-fresh2 :: ABT.V -> ABT.V -> Context -> (ABT.V, ABT.V)
+fresh2 :: Var v => v -> v -> Context v -> (v, v)
 fresh2 va vb ctx = case fresh va ctx of
   va -> (va, ABT.fresh' (Set.insert va (usedVars ctx)) vb)
 
 -- Generate three fresh variables of the given names, guaranteed fresh wrt `ctx`.
-fresh3 :: ABT.V -> ABT.V -> ABT.V -> Context -> (ABT.V, ABT.V, ABT.V)
+fresh3 :: Var v => v -> v -> v -> Context v -> (v, v, v)
 fresh3 va vb vc ctx = case fresh2 va vb ctx of
   (va, vb) -> (va, vb, ABT.fresh' (Set.insert va . Set.insert vb $ usedVars ctx) vc)
 
 -- | Extend this `Context` with a single universally quantified variable,
 -- guaranteed to be fresh
-extendUniversal :: ABT.V -> Context -> (ABT.V, Context)
+extendUniversal :: Var v => v -> Context v -> (v, Context v)
 extendUniversal v ctx = case fresh v ctx of
   v -> (v, extend (Universal v) ctx)
 
 -- | Extend this `Context` with a marker variable, guaranteed to be fresh
-extendMarker :: ABT.V -> Context -> (ABT.V, Context)
+extendMarker :: Var v => v -> Context v -> (v, Context v)
 extendMarker v ctx = case fresh v ctx of
   v -> (v, ctx `append` context [Marker v, Existential v])
 
 -- | Delete from the end of this context up to and including
 -- the given `Element`. Returns `Left` if the element is not found.
-retract :: Element -> Context -> Either Note Context
+retract :: Var v => Element v -> Context v -> Either Note (Context v)
 retract m (Context ctx) =
   let maybeTail [] = Left $ Note.note ("unable to retract: " ++ show m)
       maybeTail (_:t) = Right t
@@ -151,26 +153,26 @@ retract m (Context ctx) =
   in Context <$> maybeTail (dropWhile (\(e,_) -> e /= m) ctx)
 
 -- | Like `retract`, but returns the empty context if retracting would remove all elements.
-retract' :: Element -> Context -> Context
+retract' :: Var v => Element v -> Context v -> Context v
 retract' e ctx = case retract e ctx of
   Left _ -> context []
   Right ctx -> ctx
 
-universals :: Context -> Set ABT.V
+universals :: Context v -> Set v
 universals = universalVars . info
 
-existentials :: Context -> Set ABT.V
+existentials :: Context v -> Set v
 existentials = existentialVars . info
 
-solved :: Context -> [(ABT.V, Monotype)]
+solved :: Context v -> [(v, Monotype v)]
 solved (Context ctx) = [(v, sa) | (Solved v sa,_) <- ctx]
 
-unsolved :: Context -> [ABT.V]
+unsolved :: Context v -> [v]
 unsolved (Context ctx) = [v | (Existential v,_) <- ctx]
 
 -- | Apply the context to the input type, then convert any unsolved existentials
 -- to universals.
-generalizeExistentials :: Context -> Type -> Type
+generalizeExistentials :: Var v => Context v -> Type v -> Type v
 generalizeExistentials ctx t = foldr gen (apply ctx t) (unsolved ctx)
   where
     gen e t =
@@ -178,10 +180,10 @@ generalizeExistentials ctx t = foldr gen (apply ctx t) (unsolved ctx)
       then Type.forall e (ABT.replace (Type.universal e) (Type.matchExistential e) t)
       else t -- don't bother introducing a forall if type variable is unused
 
-replace :: Element -> Context -> Context -> Context
+replace :: Var v => Element v -> Context v -> Context v -> Context v
 replace e focus ctx = let (l,r) = breakAt e ctx in l `append` focus `append` r
 
-breakAt :: Element -> Context -> (Context, Context)
+breakAt :: Var v => Element v -> Context v -> (Context v, Context v)
 breakAt m (Context xs) =
   let (r, l) = break (\(e,_) -> e === m) xs
   -- l is a suffix of xs and is already a valid context;
@@ -189,17 +191,17 @@ breakAt m (Context xs) =
   in (Context (drop 1 l), context . map fst $ reverse r)
 
 -- | ordered Γ α β = True <=> Γ[α^][β^]
-ordered :: Context -> ABT.V -> ABT.V -> Bool
+ordered :: Var v => Context v -> v -> v -> Bool
 ordered ctx v v2 = Set.member v (existentials (retract' (Existential v2) ctx))
 
 -- | Check that the context is well formed, see Figure 7 of paper
 -- Since contexts are 'monotonic', we can compute an cache this efficiently
 -- as the context is built up, see implementation of `extend`.
-wellformed :: Context -> Bool
+wellformed :: Context v -> Bool
 wellformed ctx = isWellformed (info ctx)
 
 -- | Check that the type is well formed wrt the given `Context`, see Figure 7 of paper
-wellformedType :: Context -> Type -> Bool
+wellformedType :: Var v => Context v -> Type v -> Bool
 wellformedType c t = wellformed c && case t of
   Type.Existential' v -> Set.member v (existentials c)
   Type.Universal' v -> Set.member v (universals c)
@@ -213,16 +215,16 @@ wellformedType c t = wellformed c && case t of
     in wellformedType ctx2 (ABT.replace (Type.universal v') (Type.matchUniversal v) t)
   _ -> error $ "Context.wellformedType - ill formed type - " ++ show t
 
-bindings :: Context -> [(ABT.V, Type)]
+bindings :: Context v -> [(v, Type v)]
 bindings (Context ctx) = [(v,a) | (Ann v a,_) <- ctx]
 
-lookupType :: Context -> ABT.V -> Maybe Type
+lookupType :: Eq v => Context v -> v -> Maybe (Type v)
 lookupType ctx v = lookup v (bindings ctx)
 
 -- | solve (ΓL,α^,ΓR) α τ = (ΓL,α = τ,ΓR)
 -- If the given existential variable exists in the context,
 -- we solve it to the given monotype, otherwise return `Nothing`
-solve :: Context -> ABT.V -> Monotype -> Maybe Context
+solve :: Var v => Context v -> v -> Monotype v -> Maybe (Context v)
 solve ctx v t
   | wellformedType ctxL (Type.getPolytype t) = Just ctx'
   | otherwise                                = Nothing
@@ -230,7 +232,7 @@ solve ctx v t
         ctx' = ctxL `append` context [Solved v t] `append` ctxR
 
 -- | Replace any existentials with their solution in the context
-apply :: Context -> Type -> Type
+apply :: Var v => Context v -> Type v -> Type v
 apply ctx t = case t of
   Type.Universal' _ -> t
   Type.Lit' _ -> t
@@ -246,7 +248,7 @@ apply ctx t = case t of
 -- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
 -- This may have the effect of altering the context.
 -- see Figure 9
-subtype :: Context -> Type -> Type -> Either Note Context
+subtype :: Var v => Context v -> Type v -> Type v -> Either Note (Context v)
 subtype ctx tx ty = Note.scope (show tx++" <: "++show ty) (go tx ty) where -- Rules from figure 9
   go (Type.Lit' l) (Type.Lit' l2) | l == l2 = pure ctx -- `Unit`
   go t1@(Type.Universal' v1) t2@(Type.Universal' v2) -- `Var`
@@ -281,7 +283,7 @@ subtype ctx tx ty = Note.scope (show tx++" <: "++show ty) (go tx ty) where -- Ru
 -- | Instantiate the given existential such that it is
 -- a subtype of the given type, updating the context
 -- in the process.
-instantiateL :: Context -> ABT.V -> Type -> Either Note Context
+instantiateL :: Var v => Context v -> v -> Type v -> Either Note (Context v)
 instantiateL ctx v t = case Type.monotype t >>= solve ctx v of
   Just ctx' -> pure ctx' -- InstLSolve
   Nothing -> case t of
@@ -314,7 +316,7 @@ instantiateL ctx v t = case Type.monotype t >>= solve ctx v of
 -- | Instantiate the given existential such that it is
 -- a supertype of the given type, updating the context
 -- in the process.
-instantiateR :: Context -> Type -> ABT.V -> Either Note Context
+instantiateR :: Var v => Context v -> Type v -> v -> Either Note (Context v)
 instantiateR ctx t v = case Type.monotype t >>= solve ctx v of
   Just ctx' -> pure ctx' -- InstRSolve
   Nothing -> case t of
@@ -349,7 +351,7 @@ instantiateR ctx t v = case Type.monotype t >>= solve ctx v of
 
 -- | Check that under the given context, `e` has type `t`,
 -- updating the context in the process.
-check :: Context -> Term -> Type -> Either Note Context
+check :: Var v => Context v -> Term v -> Type v -> Either Note (Context v)
 check ctx e t | wellformedType ctx t = Note.scope ("check: " ++ show e ++ ":   " ++ show t) $ go e t where
   go (Term.Lit' l) _ = subtype ctx (synthLit l) t -- 1I
   go _ (Type.Forall' x body) = -- ForallI
@@ -384,7 +386,7 @@ check ctx e t = Note.scope ("context: " ++ show ctx) .
                 $ Left (Note.note "check failed")
 
 -- | Infer the type of a literal
-synthLit :: Term.Literal -> Type
+synthLit :: Ord v => Term.Literal -> Type v
 synthLit lit = Type.lit $ case lit of
   Term.Number _ -> Type.Number
   Term.Text _ -> Type.Text
@@ -395,7 +397,7 @@ synthLit lit = Type.lit $ case lit of
 -- their type. Also returns the freshened version of `body` and a marker
 -- which should be used to retract the context after checking/synthesis
 -- of `body` is complete. See usage in `synthesize` and `check` for `LetRec'` case.
-annotateLetRecBindings :: Context -> [(ABT.V, Term)] -> Term -> Either Note (Element, Term, Context)
+annotateLetRecBindings :: Var v => Context v -> [(v, Term v)] -> Term v -> Either Note (Element v, Term v, Context v)
 annotateLetRecBindings ctx bindings body = do
   -- freshen all the term variables `v1, v2 ...` used by each binding `b1, b2 ..`
   let vs = ABT.freshes' (usedVars ctx) (map fst bindings)
@@ -424,7 +426,7 @@ annotateLetRecBindings ctx bindings body = do
   pure $ (marker, body, ctx1 `append` context (marker : annotations))
 
 -- | Synthesize the type of the given term, updating the context in the process.
-synthesize :: Context -> Term -> Either Note (Type, Context)
+synthesize :: Var v => Context v -> Term v -> Either Note (Type v, Context v)
 synthesize ctx e = Note.scope ("synth: " ++ show e) $ go e where
   go (Term.Var' v) = case lookupType ctx v of -- Var
     Nothing -> Left $ Note.note "type not in scope"
@@ -479,7 +481,7 @@ synthesize ctx e = Note.scope ("synth: " ++ show e) $ go e where
 -- | Synthesize the type of the given term, `arg` given that a function of
 -- the given type `ft` is being applied to `arg`. Update the context in
 -- the process.
-synthesizeApp :: Context -> Type -> Term -> Either Note (Type, Context)
+synthesizeApp :: Var v => Context v -> Type v -> Term v -> Either Note (Type v, Context v)
 synthesizeApp ctx ft arg = go ft where
   go (Type.Forall' x body) = let x' = fresh x ctx -- Forall1App
     in synthesizeApp (ctx `append` context [Existential x'])
@@ -499,15 +501,14 @@ synthesizeApp ctx ft arg = go ft where
          , "function type: " ++ show ft
          , "arg: " ++ show arg ]
 
-annotateRefs :: Applicative f => Type.Env f -> Term -> Noted f Term
+annotateRefs :: (Applicative f, Ord v) => Type.Env f v -> Term v -> Noted f (Term v)
 annotateRefs synth term = ABT.visit f term where
   f (Term.Ref' h) = Just (Term.ann (Term.ref h) <$> synth h)
   f _ = Nothing
 
-synthesizeClosed :: Applicative f => Type.Env f -> Term -> Noted f Type
+synthesizeClosed :: (Applicative f, Var v) => Type.Env f v -> Term v -> Noted f (Type v)
 synthesizeClosed synthRef term = Noted $ synth <$> Note.unnote (annotateRefs synthRef term)
   where
-    synth :: Either Note Term -> Either Note Type
     synth (Left e) = Left e
     synth (Right a) = go <$> synthesize (context []) a
     go (t, ctx) = generalizeExistentials ctx t -- we generalize over any remaining unsolved existentials

shared/src/Unison/Var.hs

@@ -0,0 +1,27 @@
+module Unison.Var where
+
+import Data.Set (Set)
+import Data.Text (Text)
+import qualified Data.Set as Set
+
+class (Eq v, Ord v) => Var v where
+  named :: Text -> v
+  name :: v -> Text
+  qualifiedName :: v -> Text
+  freshIn :: Set v -> v -> v
+
+shortName :: Var v => v -> Text
+shortName v | named (name v) == v = name v
+shortName v = qualifiedName v
+
+freshes :: Var v => Set v -> [v] -> [v]
+freshes _ [] = []
+freshes used (h:t) =
+  let h' = freshIn used h
+  in h' : freshes (Set.insert h' used) t
+
+freshInBoth :: Var v => Set v -> Set v -> v -> v
+freshInBoth vs1 vs2 = freshIn vs1 . freshIn vs2
+
+freshNamed :: Var v => Set v -> Text -> v
+freshNamed used n = freshIn used (named n)

shared/unison-shared.cabal

@@ -51,6 +51,7 @@ library
     Unison.Type
     Unison.Typechecker
     Unison.Typechecker.Context
+    Unison.Var
 
   build-depends:
     aeson,