feat: *-kinded holes which are solved by BRAT

brat/Brat/Checker.hs

@@ -25,6 +25,7 @@ import Prelude hiding (filter)
 import Brat.Checker.Helpers
 import Brat.Checker.Monad
 import Brat.Checker.Quantity
+import Brat.Checker.SolveHoles (typeEq)
 import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve)
 import Brat.Checker.Types
 import Brat.Constructors
@@ -659,7 +660,13 @@ check' (Of n e) ((), unders) = case ?my of
       (elems, unders, rightUnders) <- getVecs len unders
       pure ((tgt, el):elems, (tgt, ty):unders, rightUnders)
   getVecs _ unders = pure ([], [], unders)
-
+check' Hope ((), (NamedPort hope _, ty):unders) = case (?my, ty) of
+  (Braty, Left _k) -> do
+    fc <- req AskFC
+    req (ANewHope hope fc)
+    pure (((), ()), ((), unders))
+  (Braty, Right _ty) -> typeErr "Can only infer kinded things with !"
+  (Kerny, _) -> typeErr "Won't infer kernel typed !"
 check' tm _ = error $ "check' " ++ show tm
 
 
@@ -1124,13 +1131,27 @@ run :: VEnv
     -> Namespace
     -> Checking a
     -> Either Error (a, ([TypedHole], Store, Graph))
-run ve initStore ns m =
+run ve initStore ns m = do
   let ctx = Ctx { globalVEnv = ve
                 , store = initStore
                 -- TODO: fill with default constructors
                 , constructors = defaultConstructors
                 , kconstructors = kernelConstructors
                 , typeConstructors = defaultTypeConstructors
                 , aliasTable = M.empty
-                } in
-    (\(a,ctx,(holes, graph)) -> (a, (holes, store ctx, graph))) <$> handler (localNS ns m) ctx mempty
+                , hopes = M.empty
+                }
+  (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty
+  let tyMap = typeMap $ store ctx
+  -- If the `hopes` set has any remaining holes with kind Nat, we need to abort.
+  -- Even though we didn't need them for typechecking problems, our runtime
+  -- behaviour depends on the values of the holes, which we can't account for.
+  case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap (InEnd e)) (hopes ctx) of
+    [] -> pure (a, (holes, store ctx, graph))
+    -- Just use the FC of the first hole while we don't have the capacity to
+    -- show multiple error locations
+    hs@((_,fc):_) -> Left $ Err (Just fc) (RemainingNatHopes (show . fst <$> hs))
+ where
+  isNatKinded tyMap e = case tyMap M.! e of
+    EndType Braty (Left Nat) -> True
+    _ -> False

brat/Brat/Checker/Helpers.hs

@@ -109,7 +109,7 @@
              -> Checking [(PortName, ty)]
 pullPortsSig = pullPorts fst showSig
 
 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
@@ -117,7 +117,7 @@
           -> Checking [a]
 pullPorts toPort showFn to_pull types =
   -- the "state" here is the things still available to be pulled
   (\(pulled, rest) -> pulled ++ rest) <$> runStateT (mapM pull1Port to_pull) types
  where
   pull1Port :: PortName -> StateT [a] Checking a
   pull1Port p = StateT $ \available -> case partition ((== p) . toPort) available of
@@ -306,7 +306,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 +333,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))
@@ -492,3 +492,8 @@
  -- 2^(2^k * upr) + 2^(2^k * upr) * (full(2^(k + k') * mono))
  = pure $ NumValue (upl ^ upr) (StrictMonoFun (StrictMono (l * upr) (Full (StrictMono (k + k') mono))))
 runArith _ _ _ = Nothing
+
+buildConst :: SimpleTerm -> Val Z -> Checking Src
+buildConst tm ty = do
+  (_, _, [(out,_)], _) <- next "buildConst" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0)
+  pure out

brat/Brat/Checker/Monad.hs

@@ -50,12 +50,16 @@ data CtxEnv = CtxEnv
   , locals :: VEnv
   }
 
+type Hopes = M.Map InPort FC
+
 data Context = Ctx { globalVEnv :: VEnv
                    , store :: Store
                    , constructors :: ConstructorMap Brat
                    , kconstructors :: ConstructorMap Kernel
                    , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)]
                    , aliasTable :: M.Map QualName Alias
+                   -- All the ends here should be targets
+                   , hopes :: Hopes
                    }
 
 data CheckingSig ty where
@@ -89,6 +93,9 @@ data CheckingSig ty where
   AskVEnv :: CheckingSig CtxEnv
   Declare :: End -> Modey m -> BinderType m -> CheckingSig ()
   Define  :: End -> Val Z -> CheckingSig ()
+  ANewHope :: InPort -> FC -> CheckingSig ()
+  AskHopes :: CheckingSig Hopes
+  RemoveHope :: InPort -> CheckingSig ()
 
 localAlias :: (QualName, Alias) -> Checking v -> Checking v
 localAlias _ (Ret v) = Ret v
@@ -267,6 +274,15 @@ handler (Req s k) ctx g
                 M.lookup tycon tbl
         handler (k args) ctx g
 
+      ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g
+
+      AskHopes -> handler (k (hopes ctx)) ctx g
+
+      RemoveHope e -> let hset = hopes ctx in
+                        if M.member e hset
+                        then handler (k ()) (ctx { hopes = M.delete e hset }) g
+                        else Left (dumbErr (InternalError ("Trying to remove Hope not in set: " ++ show e)))
+
 type Checking = Free CheckingSig
 
 instance Semigroup a => Semigroup (Checking a) where

brat/Brat/Checker/SolveHoles.hs

@@ -0,0 +1,160 @@
+module Brat.Checker.SolveHoles (typeEq) where
+
+import Brat.Checker.Helpers (buildConst)
+import Brat.Checker.Monad
+import Brat.Checker.Types (kindForMode)
+import Brat.Error (ErrorMsg(..))
+import Brat.Eval
+import Brat.Syntax.Common
+import Brat.Syntax.Simple (SimpleTerm(..))
+import Brat.Syntax.Value
+import Control.Monad.Freer
+import Bwd
+import Hasochism
+import Util (zipSameLength)
+
+import Data.Bifunctor (second)
+import Data.Foldable (sequenceA_)
+import Data.Functor
+import qualified Data.Map as M
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
+
+-- External interface to typeEq' for closed values only.
+typeEq :: String -- String representation of the term for error reporting
+       -> TypeKind -- The kind we're comparing at
+       -> Val Z -- Expected
+       -> Val Z -- Actual
+       -> Checking ()
+typeEq str = typeEq' str (Zy :* S0 :* S0)
+
+-- Demand that two things are equal, we're allowed to solve variables in the
+-- hope set to make this true.
+-- Raises a user error if the vals cannot be made equal.
+typeEq' :: String -- String representation of the term for error reporting
+        -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
+        -> TypeKind -- The kind we're comparing at
+        -> Val n -- Expected
+        -> Val n -- Actual
+        -> Checking ()
+typeEq' str stuff@(_ny :* _ks :* sems) k exp act = do
+  hopes <- req AskHopes
+  exp <- sem sems exp
+  act <- sem sems act
+  typeEqEta str stuff hopes k exp act
+
+isNumVar :: Sem -> Maybe SVar
+isNumVar (SNum (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v))))) = Just v
+isNumVar _ = Nothing
+
+-- Presumes that the hope set and the two `Sem`s are up to date.
+typeEqEta :: String -- String representation of the term for error reporting
+          -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
+          -> Hopes -- A map from the hope set to corresponding FCs
+          -> TypeKind -- The kind we're comparing at
+          -> Sem -- Expected
+          -> Sem -- Actual
+          -> Checking ()
+typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do
+  -- Higher kinded things
+  let nextSem = semLvl lvy
+  let xz = B0 :< nextSem
+  exp <- applySem exp xz
+  act <- applySem act xz
+  typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopes (TypeFor m ks) exp act
+-- Not higher kinded - check for flex terms
+-- (We don't solve under binders for now, so we only consider Zy here)
+-- 1. "easy" flex cases
+typeEqEta _tm (Zy :* _ks :* _sems) hopes k (SApp (SPar (InEnd e)) B0) act
+  | M.member e hopes = solveHope k e act
+typeEqEta _tm (Zy :* _ks :* _sems) hopes k exp (SApp (SPar (InEnd e)) B0)
+  | M.member e hopes = solveHope k e exp
+typeEqEta _ (Zy :* _ :* _) hopes Nat exp act
+  | Just (SPar (InEnd e)) <- isNumVar exp, M.member e hopes = solveHope Nat e act
+  | Just (SPar (InEnd e)) <- isNumVar act, M.member e hopes = solveHope Nat e exp
+-- 2. harder cases, neither is in the hope set, so we can't define it ourselves
+typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
+  exp <- quote ny exp
+  act <- quote ny act
+  case [e | (VApp (VPar (InEnd e)) _) <- [exp,act], M.member e hopes] of
+    [] -> typeEqRigid tm stuff k exp act
+    [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"
+
+-- This will update the `hopes` set, potentially invalidating things that have
+-- been eval'd.
+-- The Sem is closed, for now.
+solveHope :: TypeKind -> InPort -> Sem -> Checking ()
+solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of
+  Right () -> do
+    defineEnd (InEnd hope) v
+    dangling <- case (k, v) of
+      (Nat, VNum _v) -> err $ Unimplemented "Nat hope solving" []
+      (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
+      _ -> buildConst Unit TUnit
+    req (Wire (end dangling, kindType k, hope))
+    req (RemoveHope hope)
+  Left msg -> case v of
+    VApp (VPar (InEnd end)) B0 | hope == end -> pure ()
+    -- TODO: Not all occurrences are toxic. The end could be in an argument
+    -- to a hoping variable which isn't used.
+    -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1.
+    _ -> err msg
+
+typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking ()
+typeEqs _ _ [] [] [] = pure ()
+typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = typeEqs tm stuff ks exps acts <* typeEq' tm stuff k exp act
+typeEqs _ _ _ _ _ = typeErr "arity mismatch"
+
+typeEqRow :: Modey m
+          -> String -- The term we complain about in errors
+          -> (Ny :* Stack Z TypeKind :* Stack Z Sem) lv -- Next available level, the kinds of existing levels
+          -> Ro m lv top0
+          -> Ro m lv top1
+          -> Either ErrorMsg (Some ((Ny :* Stack Z TypeKind :* Stack Z Sem) -- The new stack of kinds and fresh level
+                                   :* ((:~:) top0 :* (:~:) top1)) -- Proofs both input rows have same length (quantified over by Some)
+                             ,[Checking ()] -- subproblems to run in parallel
+                             )
+typeEqRow _ _ stuff R0 R0 = pure (Some (stuff :* (Refl :* Refl)), [])
+typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> second
+  ((:) (typeEq' tm stuff (kindForMode m) ty1 ty2))
+typeEqRow m tm (ny :* kz :* semz) (REx (_,k1) ro1) (REx (_,k2) ro2) | k1 == k2 = typeEqRow m tm (Sy ny :* (kz :<< k1) :* (semz :<< semLvl ny)) ro1 ro2
+typeEqRow _ _ _ _ _ = Left $ TypeErr "Mismatched rows"
+
+-- Calls to typeEqRigid *must* start with rigid types to ensure termination
+typeEqRigid :: String -- String representation of the term for error reporting
+            -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
+            -> TypeKind -- The kind we're comparing at
+            -> Val n -- Expected
+            -> Val n -- Actual
+            -> Checking ()
+typeEqRigid tm (_ :* _ :* semz) Nat exp act = do
+  -- TODO: What if there's hope in the numbers?
+  exp <- sem semz exp
+  act <- sem semz act
+  if getNum exp == getNum act
+  then pure ()
+  else err $ TypeMismatch tm (show exp) (show 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' <>> [])
+      -- pattern should always match
+    _ -> err $ InternalError "quote gave a surprising result"
+ where
+  svKind (VPar e) = kindOf (VPar e)
+  svKind (VInx n) = pure $ proj kz n
+typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' =
+  req (TLup (m, c)) >>= \case
+        Just ks -> typeEqs tm lvkz (snd <$> ks) args args'
+        Nothing -> err $ TypeErr $ "Type constructor " ++ show c
+                        ++ " undefined " ++ " at kind " ++ show (TypeFor m [])
+typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 = do
+  probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg
+        (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd
+  sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
+typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1)
+  | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of
+      Nothing -> typeErr "Mismatched sum lengths"
+      Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat)
+ where
+  eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1)
+typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1)

brat/Brat/Checker/SolvePatterns.hs

@@ -19,7 +19,6 @@
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
-import Data.Foldable (for_, traverse_)
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
@@ -78,7 +77,7 @@
     (Braty, Left Nat)
       | Num n <- tm -> do
           unless (n >= 0) $ typeErr "Negative Nat kind"
-          unifyNum (nConstant (fromIntegral n)) (nVar (VPar (ExEnd (end src))))
+          unifyNum (nConstant (fromIntegral n)) (nVar (VPar (toEnd src)))
     (Braty, Right ty) -> do
       throwLeft (simpleCheck Braty ty tm)
     _ -> typeErr $ "Literal " ++ show tm ++ " isn't valid at this type"
@@ -97,7 +96,7 @@
       -- Special case for 0, so that we can call `unifyNum` instead of pattern
       -- matching using what's returned from `natConstructors`
       PrefixName [] "zero" -> do
-        unifyNum (nVar (VPar (ExEnd (end src)))) nZero
+        unifyNum (nVar (VPar (toEnd src))) nZero
         p <- argProblems [] (normaliseAbstractor abs) p
         (tests, sol) <- solve my p
         pure ((src, PrimLitTest (Num 0)):tests, sol)
@@ -108,7 +107,7 @@
             (REx ("inner", Nat) R0)
           unifyNum
            (nVar (VPar (ExEnd (end src))))
-           (relationToInner (nVar (VPar (ExEnd (end dangling)))))
+           (relationToInner (nVar (VPar (toEnd dangling))))
           p <- argProblems [dangling] (normaliseAbstractor abs) p
           (tests, sol) <- solve my p
           -- When we get @-patterns, we shouldn't drop this anymore
@@ -199,38 +198,7 @@
   defineEnd e val
 
 
--- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding
--- We can have bogus failures here because we're not normalising under lambdas
--- N.B. the value argument is normalised.
-doesntOccur :: End -> Val n -> Either ErrorMsg ()
-doesntOccur e (VNum nv) = for_ (getNumVar nv) (collision e)
  where
-  getNumVar :: NumVal (VVar n) -> Maybe End
-  getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of
-    Linear v -> case v of
-      VPar e -> Just e
-      _ -> Nothing
-    Full sm -> getNumVar (numValue sm)
-  getNumVar _ = Nothing
-doesntOccur e (VApp var args) = case var of
-  VPar e' -> collision e e' *> traverse_ (doesntOccur e) args
-  _ -> pure ()
-doesntOccur e (VCon _ args) = traverse_ (doesntOccur e) args
-doesntOccur e (VLam body) = doesntOccur e body
-doesntOccur e (VFun my (ins :->> outs)) = case my of
-  Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
-  Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
-doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows
-
-collision :: End -> End -> Either ErrorMsg ()
-collision e v | e == v = Left . UnificationError $
-                         show e ++ " is cyclic"
-              | otherwise = pure ()
-
-doesntOccurRo :: Modey m -> End -> Ro m i j -> Either ErrorMsg ()
-doesntOccurRo _ _ R0 = pure ()
-doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro
-doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro
 
 -- Need to keep track of which way we're solving - which side is known/unknown
 -- Things which are dynamically unknown must be Tgts - information flows from Srcs

brat/Brat/Elaborator.hs

@@ -91,6 +91,7 @@ elaborate (WC fc x) = do
 
 elaborate' :: Flat -> Either Error SomeRaw'
 elaborate' (FVar x) = pure $ SomeRaw' (RVar x)
+elaborate' FHope = pure $ SomeRaw' RHope
 elaborate' (FArith op a b) = do
   (SomeRaw a) <- elaborate a
   (SomeRaw b) <- elaborate b

brat/Brat/Error.hs

@@ -83,6 +83,7 @@
  -- The argument is the row of unused connectors
  | ThunkLeftOvers String
  | ThunkLeftUnders String
+ | RemainingNatHopes [String]
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -166,7 +167,7 @@
   show UnreachableBranch = "Branch cannot be reached"
   show (ThunkLeftOvers overs) = "Expected function to address all inputs, but " ++ overs ++ " wasn't used"
   show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders
-
+  show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":(("    " ++) <$> hs))
 
 data Error = Err { fc  :: Maybe FC
                  , msg :: ErrorMsg
@@ -213,8 +214,8 @@
     ls = lines contents
   in case endLineN - startLineN of
        0 -> [ls!!startLineN, highlightSection startCol endCol]
        n | n > 0 -> let (first:rest) = drop (startLineN - 1) $ take (endLineN + 1) ls
                         (last:rmid) = reverse rest
                     in [first, highlightSection startCol (length first)]
                        ++ (reverse rmid >>= (\l -> [l, highlightSection 0 (length l)]))
                        ++ [last, highlightSection 0 endCol]