feat: Human-friendly metavariable printing

brat/Brat/Checker.hs

@@ -101,6 +101,7 @@ instance CombineInputs [(Tgt, a)] where
 
 type CheckConstraints m k =
   (Show (BinderType m)
+  ,ShowWithMetas (BinderType m)
   ,TensorOutputs (Outputs m Syn)
   ,TensorOutputs (Outputs m Chk)
   ,CombineInputs (Inputs m k)
@@ -143,9 +144,10 @@ checkIO :: forall m d k exp act . (CheckConstraints m k, ?my :: Modey m)
         -> Checking [(NamedPort exp, BinderType m)] -- left(overs/unders)
 checkIO tm@(WC fc _) exps acts wireFn errMsg = modily ?my $ do
   let (rows, rest) = zipSuffixes exps acts
+  nm <- req AskNames
   localFC fc $ forM rows $ \(e:|exps, a:|acts) ->
-      wrapError (addRowContext (showRow $ e:exps) (showRow $ a:acts)) $ wireFn e a
-  throwLeft $ first (\(b:|bs) -> TypeErr $ errMsg ++ showRow (b:bs) ++ " for " ++ show tm) rest
+      wrapError (addRowContext (showRow nm $ e:exps) (showRow nm $ a:acts)) $ wireFn e a
+  throwLeft $ first (\(b:|bs) -> TypeErr $ errMsg ++ showRow nm (b:bs) ++ " for " ++ show tm) rest
  where
   addRowContext :: String -> String -> Error -> Error
   addRowContext exp act = \case
@@ -305,7 +307,9 @@ check' (Th tm) ((), u@(hungry, ty):unders) = case (?my, ty) of
       Right ty@(VFun Braty cty) -> checkThunk Braty "thunk" cty tm >>= wire . (,ty, hungry)
       Right ty@(VFun Kerny cty) -> checkThunk Kerny "thunk" cty tm >>= wire . (,ty, hungry)
       Left (Star args) -> kindCheck [(hungry, Star args)] (Th tm) $> ()
-      _ -> err . ExpectedThunk "" $ showRow (u:unders)
+      _ -> do
+        nm <- req AskNames
+        err . ExpectedThunk "" $ showRow nm (u:unders)
     pure (((), ()), ((), unders))
   (Kerny, _) -> err . ThunkInKernel $ show (Th tm)
  where
@@ -319,12 +323,13 @@ check' (Th tm) ((), u@(hungry, ty):unders) = case (?my, ty) of
     ((dangling, _), ()) <- let ?my = m in makeBox name cty $
       \(thOvers, thUnders) -> do
         (((), ()), leftovers) <- check tm (thOvers, thUnders)
+        nm <- req AskNames
         case leftovers of
           ([], []) -> pure ()
-          ([], unders) -> err (ThunkLeftUnders (showRow unders))
+          ([], unders) -> err (ThunkLeftUnders (showRow nm unders))
           -- If there are leftovers and leftunders, complain about the leftovers
           -- Until we can report multiple errors!
-          (overs, _) -> err (ThunkLeftOvers (showRow overs))
+          (overs, _) -> err (ThunkLeftOvers (showRow nm overs))
     pure dangling
 check' (TypedTh t) ((), ()) = case ?my of
   -- the thunk itself must be Braty
@@ -393,11 +398,12 @@ check' (Arith op l r) ((), u@(hungry, ty):unders) = case (?my, ty) of
 check' (fun :$: arg) (overs, unders) = do
   ((ins, outputs), ((), leftUnders)) <- check fun ((), unders)
   ((argIns, ()), (leftOvers, argUnders)) <- check arg (overs, ins)
+  nm <- req AskNames
   if null argUnders
   then pure ((argIns, outputs), (leftOvers, leftUnders))
   else typeErr $ unwords ["Expected function", show fun
                          ,"to consume all of its arguments (" ++ show arg ++ ")\n"
-                         ,"but found leftovers:", showRow argUnders
+                         ,"but found leftovers:", showRow nm argUnders
                          ]
 check' (Let abs x y) conn = do
   (((), dangling), ((), ())) <- check x ((), ())
@@ -577,9 +583,9 @@ check' (Of n e) ((), unders) = case ?my of
     ensureEmpty "" leftovers
     case diry @d of
       -- Get the largest prefix of unders whose types are vectors of the right length
-      Chky -> getVecs n unders >>= \case
+      Chky -> req AskNames >>= \nm -> getVecs n unders >>= \case
         -- If none of the unders have the right type, we should fail
-        ([], [], _) -> let expected = if null unders then "empty row" else showRow unders in
+        ([], [], _) -> let expected = if null unders then "empty row" else showRow nm unders in
                         typeErr $ unlines ["Got: Vector of length " ++ show n
                                           ,"Expected: " ++ expected]
         (elemUnders, vecUnders, rightUnders) -> do
@@ -727,6 +733,7 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
           -> CTy m Z -- Function type
           -> Checking Src
 checkBody fnName body cty = do
+  nm <- req AskNames
   (tm, (absFC, tmFC)) <- case body of
     NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
     Clauses (c@(abs, tm) :| cs) -> do
@@ -739,9 +746,9 @@ checkBody fnName body cty = do
       ([], []) -> pure ()
       ([], rightUnders) -> localFC tmFC $
         let numUsed = length unders - length rightUnders
-        in err (TypeMismatch (show tm) (showRow unders) (showRow (take numUsed unders)))
+        in err (TypeMismatch (show tm) (showRow nm unders) (showRow nm (take numUsed unders)))
       (rightOvers, _) -> localFC absFC $
-        typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
+        typeErr ("Inputs " ++ showRow nm rightOvers ++ " weren't used")
   pure src
 
 -- Constructs row from a list of ends and types. Uses standardize to ensure that dependency is
@@ -986,17 +993,18 @@ detectVecErrors :: QualName  -- Term constructor name
                 -> Val Z     -- Type
                 -> Either (Term d k) Pattern  -- Term or pattern
                 -> Checking (Error -> Error)  -- Returns error wrapper to use for recursion
-detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp =
+detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp = do
+  nm <- req AskNames
   case numMatch B0 n p of
     Left (NumMatchFail _ _) -> do
       p' <- toLenConstr p
-      err $ getVecErr tp (show ty) (show n) p'
+      err $ getVecErr tp (showWithMetas nm ty) (showWithMetas nm n) p'
     -- Even if we succed here, the error might pop up when checking the
     -- rest of the vector. We return a function here that intercepts the
     -- error and extends it to the whole vector.
     _ -> if vcon == PrefixName [] "cons"
          then do fc <- req AskFC
-                 pure (consError fc tp (show ty) n)
+                 pure (consError fc tp (showWithMetas nm ty) (showWithMetas nm n))
          else pure id
  where
   -- For constructors that produce something of type Vec we should
@@ -1013,15 +1021,15 @@ getVecErr (Left tm) = VecLength (show tm)
 getVecErr (Right pat) = VecPatLength (show pat)
 
 -- Wrapper extending an error occurring on the RHS of a cons to the whole vector
-consError :: Show v => FC -> Either (Term d k) Pattern -> String -> NumVal v -> Error -> Error
+consError :: FC -> Either (Term d k) Pattern -> String -> String -> Error -> Error
 consError fc tp ty exp err = case (tp, msg err) of
     (Left _, VecLength _ _ _ act) -> mkVecError act
     (Right _, VecPatLength _ _ _ act) -> mkVecError act
     _ -> err
  where
-  mkVecError act = Err (Just fc) $ getVecErr tp ty (show exp) ((1+) <$> act)
+  mkVecError act = Err (Just fc) $ getVecErr tp ty exp ((1+) <$> act)
 
-abstractAll :: (Show (BinderType m), EvMode m, ?my :: Modey m)
+abstractAll :: (ShowWithMetas (BinderType m), EvMode m, ?my :: Modey m)
             => [(Src, BinderType m)] -> Abstractor
             -> Checking (Env (EnvData m))
 abstractAll stuff binder = do
@@ -1030,7 +1038,7 @@ abstractAll stuff binder = do
     pure env
 
 abstract :: forall m
-          . (Show (BinderType m), ?my :: Modey m, EvMode m)
+          . (ShowWithMetas (BinderType m), ?my :: Modey m, EvMode m)
          => [(Src, BinderType m)]
          -> Abstractor
          -> Checking (Env (EnvData m) -- Local env for checking body of lambda
@@ -1048,7 +1056,7 @@ abstract ((src, ty):inputs) (APat p) = (,inputs) <$> abstractPattern ?my (src, t
 abstract [] a = err (NothingToBind (show a))
 
 abstractPattern :: forall m
-                 . (EvMode m, Show (BinderType m))
+                 . (EvMode m, ShowWithMetas (BinderType m))
                 => Modey m
                 -> (Src, BinderType m)
                 -> Pattern

brat/Brat/Checker/Helpers.hs

@@ -27,6 +27,7 @@
 import Brat.FC (FC)
 import Brat.Graph (Node(..), NodeType(..))
 import Brat.Naming (Name, FreshMonad(..))
+import Brat.QualName (QualName)
 import Brat.Syntax.Common
 import Brat.Syntax.Core (Term(..))
 import Brat.Syntax.Simple
@@ -40,9 +41,10 @@
 import Control.Monad.Freer (req)
 import Data.Bifunctor
 import Data.Foldable (foldrM)
-import Data.List (partition)
+import Data.List (intercalate, partition)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import qualified Data.Map as M
+import qualified Data.Set as S
 import Prelude hiding (last)
 
 simpleCheck :: Modey m -> Val Z -> SimpleTerm -> Either ErrorMsg ()
@@ -67,8 +69,10 @@
 -- TODO: Make an `Error` constructor for this
 pull1PortRo _ p _ R0 = fail $ "Port not found: " ++ p
 pull1PortRo m p stuff (RPr (p', ty) ro)
- | p == p' = if portNameExists m p ro
-   then err (AmbiguousPortPull p (show (RPr (p', ty) ro)))
+ | p == p' = do
+   names <- req AskNames
+   if portNameExists m p ro
+   then err (AmbiguousPortPull p (showWithMetas names (RPr (p', ty) ro)))
    else pure ((p', ty), rebuildRo m ro (stuff <>> []))
  | otherwise = pull1PortRo m p (stuff :< (p', ty)) ro
  where
@@ -97,19 +101,19 @@
   (x, ro) <- pull1PortRo m p B0 ro
   RPr x <$> pullPortsRo m ps ro
 
-pullPortsRow :: Show ty
+pullPortsRow :: ShowWithMetas ty
              => [PortName]
              -> [(NamedPort e, ty)]
              -> Checking [(NamedPort e, ty)]
-pullPortsRow = pullPorts (portName . fst) showRow
+pullPortsRow ps row = req AskNames >>= \nm -> pullPorts (portName . fst) (showRow nm) ps row
 
-pullPortsSig :: Show ty
+pullPortsSig :: ShowWithMetas ty
              => [PortName]
              -> [(PortName, ty)]
              -> Checking [(PortName, ty)]
-pullPortsSig = pullPorts fst showSig
+pullPortsSig ps row = req AskNames >>= \nm -> pullPorts fst (showSig (showWithMetas nm)) ps row
 
 pullPorts :: forall a ty
            . (a -> PortName) -- A way to get a port name for each element
           -> ([a] -> String) -- A way to print the list
           -> [PortName] -- Things to pull to the front
@@ -125,18 +129,25 @@
       ([found], remaining) -> pure (found, remaining)
       (_, _) -> err $ AmbiguousPortPull p (showFn available)
 
-ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
+combineDisjointEnvs :: M.Map QualName v -> M.Map QualName v -> Checking (M.Map QualName v)
+combineDisjointEnvs l r =
+  let commonKeys = S.intersection (M.keysSet l) (M.keysSet r)
+  in if S.null commonKeys
+    then pure $ M.union l r
+    else typeErr ("Variable(s) defined twice: " ++
+      intercalate "," (map show $ S.toList commonKeys))
+
+ensureEmpty :: ShowWithMetas ty => String -> [(NamedPort e, ty)] -> Checking ()
 ensureEmpty _ [] = pure ()
-ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showSig (rowToSig xs)
+ensureEmpty str xs = do
+  nm <- req AskNames
+  err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showRow nm xs
 
 noUnders m = do
   ((outs, ()), (overs, unders)) <- m
   ensureEmpty "unders" unders
   pure (outs, overs)
 
-rowToSig :: Traversable t => t (NamedPort e, ty) -> t (PortName, ty)
-rowToSig = fmap $ first portName
-
 showMode :: Modey m -> String
 showMode Braty = ""
 showMode Kerny = "(kernel) "
@@ -265,7 +276,9 @@
       pure (node, unders, overs)
   (nodes, unders', overs') <- getThunks Braty rest
   pure (node:nodes, unders <> unders', overs <> overs')
-getThunks m ro = err $ ExpectedThunk (showMode m) (showRow ro)
+getThunks m ro = do
+  nm <- req AskNames
+  err $ ExpectedThunk (showMode m) (showRow nm ro)
 
 -- The type given here should be normalised
 vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vector layers
@@ -306,7 +319,7 @@
     pure src
 
   mkMono :: Monotone (VVar Z) -> Checking Src
   mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono")
   mkMono (Full sm) = do
     (_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
     (_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0))
@@ -333,7 +346,7 @@
             -> (Src, CTy m Z) -- The input to this level of mapfun
             -> Checking (Src, CTy m Z)
   mkMapFun (lenSrc, len) (valSrc, cty) = do
     let weak1 = changeVar (Thinning (ThDrop ThNull))
     vecFun <- vectorisedFun len my cty
     (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right (VFun my' cty))], _) <-
       next "MapFun" MapFun (S0, Some (Zy :* S0))
@@ -382,10 +395,12 @@
 defineTgt tgt = defineEnd (InEnd (end tgt))
 
 declareSrc :: Src -> Modey m -> BinderType m -> Checking ()
-declareSrc src my ty = req (Declare (ExEnd (end src)) my ty)
+declareSrc (NamedPort end name) my ty = req (Declare (ExEnd end) my ty) *>
+                                        req (NameMeta (ExEnd end) name)
 
 declareTgt :: Tgt -> Modey m -> BinderType m -> Checking ()
-declareTgt tgt my ty = req (Declare (InEnd (end tgt)) my ty)
+declareTgt (NamedPort end name) my ty = req (Declare (InEnd end) my ty) *>
+                                        req (NameMeta (InEnd end) name)
 
 -- listToRow :: [(PortName, BinderType m)] -> Ro m Z i
 -- listToRow [] = R0

brat/Brat/Checker/Monad.hs

@@ -95,6 +95,8 @@ data CheckingSig ty where
   ANewHope :: InPort -> FC -> CheckingSig ()
   AskHopes :: CheckingSig Hopes
   RemoveHope :: InPort -> CheckingSig ()
+  NameMeta :: End -> String -> CheckingSig ()
+  AskNames :: CheckingSig (M.Map End String)
 
 localAlias :: (QualName, Alias) -> Checking v -> Checking v
 localAlias _ (Ret v) = Ret v
@@ -281,6 +283,12 @@ handler (Req s k) ctx g
                         if M.member e hset
                         then handler (k ()) (ctx { hopes = M.delete e hset }) g
                         else Left (dumbErr (InternalError ("Trying to remove unknown Hope: " ++ show e)))
+      NameMeta end name -> let names = userNames (store ctx) in
+                             case M.lookup end names of
+                               Just oldName -> error $ "Trying to name end (" ++ show end ++ ")\nas " ++ show name ++ " but it's already called " ++ oldName
+                               Nothing -> let st = store ctx in
+                                            handler (k ()) (ctx { store = st { userNames = M.insert end name (userNames st) } }) g
+      AskNames -> handler (k (userNames (store ctx))) ctx g
 
 type Checking = Free CheckingSig
 

brat/Brat/Checker/SolveHoles.hs

@@ -83,8 +83,11 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
   when (or [M.member ie hopes | InEnd ie <- ends]) $ typeErr "ends were in hopeset"
   case ends of
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
-    [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined
-    _es -> error "TODO: must wait for one or the other to become more defined"
+    -- variables are trivially the same, even if undefined, but the values may
+    -- be different! E.g. X =? 1 + X
+    [_, _] | exp == act -> pure ()
+    -- TODO: Once we have scheduling, we must wait for one or the other to become more defined, rather than failing
+    _  -> err (TypeMismatch tm (show exp) (show act))
  where
   getEnd (VApp (VPar e) _) = Just e
   getEnd (VNum n) = getNumVar n
@@ -143,7 +146,9 @@ typeEqRigid tm (_ :* _ :* semz) Nat exp act = do
   act <- sem semz act
   if getNum exp == getNum act
   then pure ()
-  else err $ TypeMismatch tm (show exp) (show act)
+  else do
+    names <- req AskNames
+    err $ TypeMismatch tm (showWithMetas names exp) (showWithMetas names act)
 typeEqRigid tm stuff@(_ :* kz :* _) (TypeFor m []) (VApp f args) (VApp f' args') | f == f' =
   svKind f >>= \case
     TypeFor m' ks | m == m' -> typeEqs tm stuff (snd <$> ks) (args <>> []) (args' <>> [])

brat/Brat/Checker/SolvePatterns.hs

@@ -193,6 +193,9 @@ unify l k r = do
 
 -- Solve a metavariable statically - don't do anything dynamic
 -- Once a metavariable is solved, we expect to not see it again in a normal form.
+--
+-- N.B. We should try harder to preserve order here for more comprehensible
+-- error messages. See the Helium/Top projects.
 instantiateMeta :: End -> Val Z -> Checking ()
 instantiateMeta e val = do
   throwLeft (doesntOccur e val)
@@ -252,7 +255,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
   demandSucc (StrictMono k (Full nPlus1)) = do
     n <- demandSucc nPlus1
     pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes (k + 1) $ nFull n
-  demandSucc n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be a successor"
+  demandSucc n = req AskNames >>= \nm -> err (UnificationError $ "Couldn't force " ++ showWithMetas nm n ++ " to be a successor")
 
   -- Complain if a number isn't even, otherwise return half
   demandEven :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))

brat/Brat/Checker/Types.hs

@@ -78,13 +78,13 @@ data HoleData a = HoleData
   , connectors :: a
   }
 
-instance Show TypedHole where
-  show (TypedHole tag dat) = ((('?' : mnemonic dat) ++ " :: ") ++) $
+instance ShowWithMetas TypedHole where
+  showWithMetas m (TypedHole tag dat) = ((('?' : mnemonic dat) ++ " :: ") ++) $
     case (tag, connectors dat) of
-      (NBHole, ((), unders)) -> showRow unders
-      (NKHole, ((), unders)) -> showRow unders
-      (VBHole, (overs, unders)) -> "{ " ++ showRow overs ++ " -> " ++ showRow unders ++ " }"
-      (VKHole, (overs, unders)) -> "{ " ++ showRow overs ++ " -o " ++ showRow unders ++ " }"
+      (NBHole, ((), unders)) -> showRow m unders
+      (NKHole, ((), unders)) -> showRow m unders
+      (VBHole, (overs, unders)) -> "{ " ++ showRow m overs ++ " -> " ++ showRow m unders ++ " }"
+      (VKHole, (overs, unders)) -> "{ " ++ showRow m overs ++ " -o " ++ showRow m unders ++ " }"
 
 data EndType where
   EndType :: Modey m -> BinderType m -> EndType
@@ -95,23 +95,25 @@ instance Show EndType where
   show (EndType Braty (Right ty)) = show ty
 
 data Store = Store
-  { typeMap  :: M.Map End EndType
-  , valueMap :: M.Map End (Val Z)
+  { typeMap    :: M.Map End EndType
+  , valueMap   :: M.Map End (Val Z)
+  , userNames  :: M.Map End String
   }
 
 instance Show Store where
-  show (Store km vm) = unlines $
+  show (Store km vm nm) = unlines $
                        ("Kinds:":(showKind <$> M.toList km))
-                       ++ ("\nValues:":(showVal <$> M.toList vm))
+                       ++ ("\nValues:":(showVal <$> M.toList vm)
+                       ++ ("\nNames:":(show <$> M.toList nm)))
    where
     showKind (key, kind) = show key ++ " :: " ++ show kind
     showVal (key, val) = show key ++ " = " ++ show val
 
 initStore :: Store
-initStore = Store M.empty M.empty
+initStore = Store M.empty M.empty M.empty
 
 instance Semigroup Store where
-  (Store ks vs) <> (Store ks' vs') = Store (ks <> ks') (vs <> vs')
+  (Store ks vs nm) <> (Store ks' vs' nm') = Store (ks <> ks') (vs <> vs') (nm <> nm')
 
 kindForMode :: Modey m -> TypeKind
 kindForMode Braty = Star []