Introduce Stuck neutral constructor

src/Core/Domain.hs

@@ -28,6 +28,7 @@ import Var (Var)
 
 data Value
   = Neutral !Head Spine
+  | Stuck !Head Args !Value Spine
   | Con !Name.QualifiedConstructor (Tsil (Plicity, Value))
   | Lit !Literal
   | Glued !Head Spine !Value
@@ -44,6 +45,17 @@ data Head
   | Meta !Meta.Index
   deriving (Show, Eq, Generic, Hashable)
 
+anyNeutralView :: Value -> Maybe (Head, Spine)
+anyNeutralView = \case
+  Neutral hd spine -> Just (hd, spine)
+  Stuck hd args _ spine -> Just (hd, Apps args <> spine)
+  _ -> Nothing
+
+pattern AnyNeutral :: Head -> Spine -> Value
+pattern AnyNeutral hd spine <- (anyNeutralView -> Just (hd, spine))
+
+{-# COMPLETE AnyNeutral, Con, Lit, Glued, Core.Domain.Lazy, Lam, Pi, Fun #-}
+
 type Environment = Environment.Environment Value
 
 data Closure where

src/Core/Domain/Showable.hs

@@ -19,6 +19,7 @@ import Protolude hiding (IntMap, Type, force, to)
 
 data Value
   = Neutral !Domain.Head Spine
+  | Stuck !Domain.Head (Seq (Plicity, Value)) Value Spine
   | Con !Name.QualifiedConstructor (Tsil (Plicity, Value))
   | Lit !Literal
   | Glued !Domain.Head Spine !Value
@@ -54,6 +55,8 @@ to value =
   case value of
     Domain.Neutral hd spine ->
       Neutral hd <$> Domain.mapM eliminationTo spine
+    Domain.Stuck hd args value' spine ->
+      Stuck hd <$> mapM (mapM to) args <*> to value' <*> Domain.mapM eliminationTo spine
     Domain.Con con args ->
       Con con <$> mapM (mapM to) args
     Domain.Lit lit ->

src/Core/Evaluation.hs

@@ -207,6 +207,8 @@ apply fun plicity arg =
           panic "Core.Evaluation: plicity mismatch"
     Domain.Neutral hd spine ->
       pure $ Domain.Neutral hd $ spine Domain.:> Domain.App plicity arg
+    Domain.Stuck hd args value spine ->
+      pure $ Domain.Stuck hd args value $ spine Domain.:> Domain.App plicity arg
     Domain.Glued hd spine value -> do
       appliedValue <- apply value plicity arg
       pure $ Domain.Glued hd (spine Domain.:> Domain.App plicity arg) appliedValue
@@ -229,6 +231,8 @@ case_ scrutinee branches@(Domain.Branches env branches' defaultBranch) =
       chooseLiteralBranch env lit literalBranches defaultBranch
     (Domain.Neutral head spine, _) ->
       pure $ Domain.Neutral head $ spine Domain.:> Domain.Case branches
+    (Domain.Stuck head args value spine, _) ->
+      pure $ Domain.Stuck head args value $ spine Domain.:> Domain.Case branches
     (Domain.Glued hd spine value, _) -> do
       casedValue <- case_ value branches
       pure $ Domain.Glued hd (spine Domain.:> Domain.Case branches) casedValue

src/Core/Readback.hs

@@ -20,7 +20,7 @@ import qualified Telescope
 readback :: Domain.Environment v -> Domain.Value -> M (Syntax.Term v)
 readback env value =
   case value of
-    Domain.Neutral head spine ->
+    Domain.AnyNeutral head spine ->
       case head of
         Domain.Var v ->
           case (Environment.lookupVarIndex v env, Environment.lookupVarValue v env) of

src/Core/TypeOf.hs

@@ -27,7 +27,7 @@ import qualified Telescope
 typeOf :: Context v -> Domain.Value -> M Domain.Type
 typeOf context value =
   case value of
-    Domain.Neutral hd spine -> do
+    Domain.AnyNeutral hd spine -> do
       headType <- typeOfHead context hd
       typeOfSpineApplication context headType spine
     Domain.Lit lit ->

src/Elaboration.hs

@@ -1021,11 +1021,11 @@ getExpectedTypeName
 getExpectedTypeName context type_ = do
   type' <- Context.forceHead context type_
   case type' of
-    Domain.Neutral (Domain.Meta blockingMeta) _ ->
+    Domain.AnyNeutral (Domain.Meta blockingMeta) _ ->
       pure $ Just $ Left blockingMeta
-    Domain.Neutral (Domain.Global name) _ ->
+    Domain.AnyNeutral (Domain.Global name) _ ->
       pure $ Just $ Right name
-    Domain.Neutral (Domain.Var _) _ ->
+    Domain.AnyNeutral (Domain.Var _) _ ->
       pure Nothing
     Domain.Con {} ->
       pure Nothing

src/Elaboration/Context.hs

@@ -315,7 +315,7 @@ freeVars
 freeVars context value = do
   value' <- lift $ forceHeadGlue context value
   case value' of
-    Domain.Neutral hd spine -> do
+    Domain.AnyNeutral hd spine -> do
       hdVars <- headVars hd
       elimVars <- Domain.mapM eliminationVars spine
       pure $ hdVars <> fold elimVars
@@ -696,6 +696,8 @@ forceHead context value =
           forceHead context value''
         Nothing ->
           pure value
+    Domain.Stuck head_ args value' spine ->
+      undefined -- TODO
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
@@ -720,6 +722,8 @@ forceHeadGlue context value =
           pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
         Nothing ->
           pure value
+    Domain.Stuck head_ args value' spine ->
+      undefined -- TODO
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHeadGlue context value'

src/Elaboration/Equation.hs

@@ -70,7 +70,7 @@ equateM flexibility unforcedValue1 unforcedValue2 = go unforcedValue1 unforcedVa
         (_, Domain.Glued _ _ value2'') ->
           go value1' value2''
         -- Same heads
-        (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
+        (Domain.AnyNeutral head1 spine1, Domain.AnyNeutral head2 spine2)
           | head1 == head2 -> do
               let flexibility' = max (Domain.headFlexibility head1) flexibility
               equateSpines flexibility' spine1 spine2
@@ -91,7 +91,7 @@ equateM flexibility unforcedValue1 unforcedValue2 = go unforcedValue1 unforcedVa
               equateM flexibility target1 target2
 
         -- Neutrals
-        (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
+        (Domain.AnyNeutral head1 spine1, Domain.AnyNeutral head2 spine2)
           | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
           , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility -> do
               -- TODO: check both directions?
@@ -100,10 +100,10 @@ equateM flexibility unforcedValue1 unforcedValue2 = go unforcedValue1 unforcedVa
                 LT -> solve head2 spine2 unforcedValue1
                 GT -> solve head1 spine1 unforcedValue2
                 EQ -> solve head2 spine2 unforcedValue1
-        (Domain.Neutral head1 spine1, _)
+        (Domain.AnyNeutral head1 spine1, _)
           | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
               solve head1 spine1 unforcedValue2
-        (_, Domain.Neutral head2 spine2)
+        (_, Domain.AnyNeutral head2 spine2)
           | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
               solve head2 spine2 unforcedValue1
         _ ->
@@ -151,7 +151,7 @@ occurs :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Value -> M
 occurs context occ flexibility value = do
   value' <- Context.forceHeadGlue context value
   case value' of
-    Domain.Neutral hd spine -> do
+    Domain.AnyNeutral hd spine -> do
       occursHead occ flexibility hd
       occursSpine context occ (max (Domain.headFlexibility hd) flexibility) spine
     Domain.Con _ args ->

src/Elaboration/Matching.hs

@@ -343,7 +343,7 @@ uncoveredScrutineePatterns
 uncoveredScrutineePatterns context value = do
   value' <- Context.forceHead context value
   case value' of
-    Domain.Neutral head_ spine -> do
+    Domain.AnyNeutral head_ spine -> do
       covered <- Context.coveredConstructors context head_ spine
       case HashSet.toList covered of
         [] ->
@@ -467,12 +467,12 @@ simplifyMatch context canPostpone match@(Match value forcedValue plicity pat typ
               pure []
           | otherwise ->
               fail "Literal mismatch"
-        (Domain.Neutral head_ spine, Con _ constr _) -> do
+        (Domain.AnyNeutral head_ spine, Con _ constr _) -> do
           covered <- lift $ Context.coveredConstructors context head_ spine
           if HashSet.member constr covered
             then fail "Constructor already covered"
             else pure [match']
-        (Domain.Neutral head_ spine, Lit lit) -> do
+        (Domain.AnyNeutral head_ spine, Lit lit) -> do
           covered <- lift $ Context.coveredLiterals context head_ spine
           if HashSet.member lit covered
             then fail "Literal already covered"
@@ -648,9 +648,9 @@ splitConstructorOr context config matches canPostpone k =
         Match _ (Domain.Neutral (Domain.Meta _) _) _ _ _
           | Postponement.CanPostpone <- canPostpone ->
               splitConstructorOr context config matches' canPostpone k
-        Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Con _ constr _)) type_ ->
+        Match scrutinee (Domain.AnyNeutral head_ spine) _ (Pattern span (Con _ constr _)) type_ ->
           splitConstructor context config scrutinee head_ spine span constr type_
-        Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Lit lit)) type_ ->
+        Match scrutinee (Domain.AnyNeutral head_ spine) _ (Pattern span (Lit lit)) type_ ->
           splitLiteral context config scrutinee head_ spine span lit type_
         _ ->
           splitConstructorOr context config matches' canPostpone k
@@ -813,7 +813,7 @@ findConstructorMatches context head_ spine matches =
   case matches of
     [] ->
       pure []
-    Match _ (Domain.Neutral head' spine') _ (Pattern _ (Con span constr patterns)) _ : matches'
+    Match _ (Domain.AnyNeutral head' spine') _ (Pattern _ (Con span constr patterns)) _ : matches'
       | head_ == head' -> do
           eq <- Unification.equalSpines context spine spine'
           if eq
@@ -868,7 +868,7 @@ findLiteralMatches context head_ spine matches =
   case matches of
     [] ->
       pure []
-    Match _ (Domain.Neutral head' spine') _ (Pattern span (Lit lit)) _ : matches'
+    Match _ (Domain.AnyNeutral head' spine') _ (Pattern span (Lit lit)) _ : matches'
       | head_ == head' -> do
           eq <- Unification.equalSpines context spine spine'
           if eq
@@ -893,7 +893,7 @@ splitEqualityOr context config matches k =
       case match of
         Match
           scrutineeValue
-          scrutineeValue'@Domain.Neutral {}
+          scrutineeValue'@Domain.AnyNeutral {}
           _
           (Pattern _ Wildcard)
           (Builtin.Equals type_ value1 value2) -> do

src/Elaboration/Unification.hs

@@ -94,7 +94,7 @@ unify context flexibility unforcedValue1 unforcedValue2 = catchAndAdd $ go unfor
         (_, Domain.Glued _ _ value2'') ->
           go value1' value2''
         -- Both metas
-        (Domain.Neutral (Domain.Meta metaIndex1) (Domain.Apps args1), Domain.Neutral (Domain.Meta metaIndex2) (Domain.Apps args2))
+        (Domain.AnyNeutral (Domain.Meta metaIndex1) (Domain.Apps args1), Domain.AnyNeutral (Domain.Meta metaIndex2) (Domain.Apps args2))
           | Flexibility.Rigid <- flexibility -> do
               args1' <- mapM (mapM $ Context.forceHead context) args1
               args2' <- mapM (mapM $ Context.forceHead context) args2
@@ -133,7 +133,7 @@ unify context flexibility unforcedValue1 unforcedValue2 = catchAndAdd $ go unfor
                       can'tUnify
 
         -- Same heads
-        (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
+        (Domain.AnyNeutral head1 (Domain.Apps args1), Domain.AnyNeutral head2 (Domain.Apps args2))
           | head1 == head2
           , (fst <$> args1) == (fst <$> args2) -> do
               let flexibility' =
@@ -222,13 +222,13 @@ unify context flexibility unforcedValue1 unforcedValue2 = catchAndAdd $ go unfor
           | Flexibility.Rigid <- flexibility -> do
               matches <- potentiallyMatchingBranches context value1' branches
               invertCase meta spine args matches
-        (Domain.Neutral head1 spine1@(Domain.Spine args1 ((branches1, _) Seq.:<| _)), Domain.Neutral head2 spine2)
+        (Domain.AnyNeutral head1 spine1@(Domain.Spine args1 ((branches1, _) Seq.:<| _)), Domain.AnyNeutral head2 spine2)
           | head1 == head2 ->
               unifySpines context Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error.Elaboration) ->
                 withBranches context head1 args1 branches1 \context' -> unify context' flexibility value1' value2
-        (Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _)), _) ->
+        (Domain.AnyNeutral head (Domain.Spine args ((branches, _) Seq.:<| _)), _) ->
           withBranches context head args branches \context' -> unify context' flexibility value1' value2
-        (_, Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _))) ->
+        (_, Domain.AnyNeutral head (Domain.Spine args ((branches, _) Seq.:<| _))) ->
           withBranches context head args branches \context' -> unify context' flexibility value1 value2'
         -- Failure terms mean that there has been an earlier error that's already
         -- been reported, so let's not trigger more errors from them.
@@ -575,10 +575,10 @@ potentiallyMatchingBranches outerContext resultValue (Domain.Branches outerEnv b
           case (body'', resultValue') of
             (Domain.Neutral (Domain.Meta _) (Domain.Apps _), _) ->
               pure True
-            (Domain.Neutral _ (_ Domain.:> Domain.Case branches'), _) -> do
+            (Domain.AnyNeutral _ (_ Domain.:> Domain.Case branches'), _) -> do
               matches <- potentiallyMatchingBranches context resultValue branches'
               pure $ not $ null matches
-            (Domain.Neutral head1 (Domain.Apps _), Domain.Neutral head2 (Domain.Apps _)) ->
+            (Domain.AnyNeutral head1 (Domain.Apps _), Domain.AnyNeutral head2 (Domain.Apps _)) ->
               pure $ head1 == head2
             (Domain.Con con1 _, Domain.Con con2 _) ->
               pure $ con1 == con2
@@ -655,7 +655,7 @@ shouldKeepMetaArgument value1 value2 =
       case value of
         Domain.Con _ Tsil.Empty ->
           True
-        Domain.Neutral hd Domain.Empty ->
+        Domain.AnyNeutral hd Domain.Empty ->
           case hd of
             Domain.Var _ ->
               False
@@ -744,15 +744,15 @@ renameValue
 renameValue outerContext renaming value = do
   value' <- Context.forceHeadGlue outerContext value
   case value' of
-    Domain.Neutral (Domain.Var var) spine ->
+    Domain.AnyNeutral (Domain.Var var) spine ->
       case Environment.lookupVarIndex var $ environment renaming of
         Nothing ->
           throwIO $ Error.TypeMismatch mempty
         Just i ->
           renameSpine outerContext renaming (Syntax.Var i) spine
-    Domain.Neutral (Domain.Global global) spine ->
+    Domain.AnyNeutral (Domain.Global global) spine ->
       renameSpine outerContext renaming (Syntax.Global global) spine
-    Domain.Neutral (Domain.Meta meta) spine
+    Domain.AnyNeutral (Domain.Meta meta) spine
       | Just meta == occurs renaming ->
           throwIO $ Error.OccursCheck mempty
       | otherwise ->