feat!: saturated constructors stage 3

primer-service/test/outputs/OpenAPI/openapi.json

@@ -170,7 +170,6 @@
             },
             "InputAction": {
                 "enum": [
-                    "MakeCon",
                     "MakeConSat",
                     "MakeInt",
                     "MakeChar",
@@ -1063,7 +1062,6 @@
                         "required": true,
                         "schema": {
                             "enum": [
-                                "MakeCon",
                                 "MakeConSat",
                                 "MakeInt",
                                 "MakeChar",

primer/gen/Primer/Gen/Core/Typed.hs

@@ -79,7 +79,6 @@ import Primer.TypeDef (
   ValCon (..),
   typeDefKind,
   typeDefParameters,
-  valConType,
  )
 import Primer.Typecheck (
   Cxt (),
@@ -234,17 +233,12 @@ genSyns ty = do
       let locals' = map (first (Var () . LocalVarRef)) $ M.toList localTms
       globals <- asks globalCxt
       let globals' = map (first (Var () . GlobalVarRef)) $ M.toList globals
-      -- TODO (saturated constructors) when saturation is enforced, constructors should not appear on the left of an app node
-      cons <- asks allCons
-      let cons' = map (first (\c -> Con () c [] [])) $ M.toList cons
-      let hsPure = locals' ++ globals' ++ cons'
-      primCons <- fmap (bimap (PrimCon ()) (TCon ())) <<$>> genPrimCon
-      let hs = map pure hsPure ++ primCons
+      let hs = locals' ++ globals'
       pure $
         if null hs
           then Nothing
           else Just $ do
-            (he, hT) <- Gen.choice hs
+            (he, hT) <- Gen.element hs
             cxt <- ask
             runExceptT (refine cxt ty hT) >>= \case
               -- This error case indicates a bug. Crash and fail loudly!
@@ -275,7 +269,7 @@ genSyns ty = do
     genCon =
       instantiateValCons ty >>= \case
         Left TDIHoleType ->
-          asks allCons' <&> \case
+          asks allCons <&> \case
             -- We have no constraints, generate any ctor
             m | null m -> Nothing
             cons -> Just $ do
@@ -390,24 +384,14 @@ genSyn :: GenT WT (ExprG, TypeG)
 -- of any type
 genSyn = genSyns (TEmptyHole ())
 
-allCons :: Cxt -> M.Map ValConName (Type' ())
-allCons cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt
-  where
-    consForTyDef tc = \case
-      TypeDefAST td -> map (\vc -> (valConName vc, valConType tc td vc)) (astTypeDefConstructors td)
-      TypeDefPrim _ -> []
-
--- TODO (saturated constructors) when saturation is enforced, allCons should be
--- no longer needed, and we can rename allCons'
-
 -- | Returns each ADT constructor's name along with its "telescope" of arguments:
 --  - the parameters of the datatype (which are type arguments to the constructor)
 --  - the types of its fields (and the names of the parameters scope over this)
 --  - the ADT it belongs to (if @c@ maps to @([(p1,k1),(p2,k2)],_,T)@ in the
 --    returned map, then @c [A,B] _ ∈ T A B@ for any @A@ of kind @k1@ and @B@
 --    of kind @k2@)
-allCons' :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName)
-allCons' cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt
+allCons :: Cxt -> M.Map ValConName ([(TyVarName, Kind)], [Type' ()], TyConName)
+allCons cxt = M.fromList $ concatMap (uncurry consForTyDef) $ M.assocs $ typeDefs cxt
   where
     consForTyDef tc = \case
       TypeDefAST td ->

primer/src/Primer/Action.hs

@@ -69,7 +69,6 @@ import Primer.Core.DSL (
   branch,
   case_,
   con,
-  con0,
   emptyHole,
   hole,
   lAM,
@@ -350,7 +349,6 @@ applyAction' a = case a of
   RemoveAnn -> termAction removeAnn "there are no annotations in types"
   ConstructLam x -> termAction (constructLam x) "cannot construct function in type"
   ConstructLAM x -> termAction (constructLAM x) "cannot construct function in type"
-  ConstructCon c -> termAction (constructCon c) "cannot construct con in type"
   ConstructPrim p -> termAction (constructPrim p) "cannot construct primitive literal in type"
   ConstructSaturatedCon c -> termAction (constructSatCon c) "cannot construct con in type"
   ConstructRefinedCon c -> termAction (constructRefinedCon c) "cannot construct con in type"
@@ -614,12 +612,6 @@ constructLAM mx ze = do
   result <- flip replace ze <$> lAM x (pure (target ze))
   moveExpr Child1 result
 
--- TODO (saturated constructors) this action will make no sense once full-saturation is enforced
-constructCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ
-constructCon c ze = case target ze of
-  EmptyHole{} -> flip replace ze <$> con0 (unsafeMkGlobalName c)
-  e -> throwError $ NeedEmptyHole (ConstructCon c) e
-
 constructPrim :: ActionM m => PrimCon -> ExprZ -> m ExprZ
 constructPrim p ze = case target ze of
   EmptyHole{} -> flip replace ze <$> prim p
@@ -667,14 +659,19 @@ constructRefinedCon c ze = do
   case target ze of
     EmptyHole{} ->
       breakLR <<$>> getRefinedApplications cxt cTy tgtTy >>= \case
+        Just (Just (tys, tms))
+          | length tys == numTyArgs && length tms == numTmArgs ->
+              flip replace ze <$> con n (pure <$> tys) (pure <$> tms)
+          -- If the refinement is not saturated, just give a saturated constructor
+          -- This could happen when refining @Cons@ to fit in a hole of type @List Nat -> List Nat@
+          -- as we get the "type" of @Cons@ being @∀a. a -> List a -> List a@
+          -- and thus a refinement of @Nat, _@.
+          | otherwise -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole))
         -- See Note [No valid refinement]
         Nothing -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole))
         -- TODO (saturated constructors): when constructors are checkable the above will not be valid
         -- since the inside of a hole must be synthesisable (see Note [Holes and bidirectionality])
-        -- TODO (saturated constructors): when saturation is enforced, the Just Just case may not be valid
-        -- if the target type is not an applied-ADT
         Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions"
-        Just (Just (tys, tms)) -> flip replace ze <$> con n (pure <$> tys) (pure <$> tms)
     e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e
 
 getTypeCache :: MonadError ActionError m => Expr -> m TypeCache
@@ -971,9 +968,6 @@ toProgActionInput ::
   Available.InputAction ->
   Either ActionError [ProgAction]
 toProgActionInput def defName mNodeSel opt0 = \case
-  Available.MakeCon -> do
-    opt <- optGlobal
-    toProg [ConstructCon opt]
   Available.MakeConSat -> do
     ref <- offerRefined
     opt <- optGlobal

primer/src/Primer/Action/Actions.hs

@@ -58,8 +58,6 @@ data Action
     ConstructLam (Maybe Text)
   | -- | Construct a type abstraction "big-lambda"
     ConstructLAM (Maybe Text)
-  | -- | Put a constructor in an empty hole
-    ConstructCon QualifiedText
   | -- | Put a literal in an empty hole
     ConstructPrim PrimCon
   | -- | Put a constructor applied to a saturated spine in an empty hole

primer/src/Primer/Action/Available.hs

@@ -122,8 +122,7 @@ data NoInputAction
 
 -- | An action which requires extra data (often a name) before it can be applied.
 data InputAction
-  = MakeCon
-  | MakeConSat
+  = MakeConSat
   | MakeInt
   | MakeChar
   | MakeVar
@@ -202,14 +201,13 @@ forExpr tydefs l expr =
     EmptyHole{} ->
       annotate
         <> [ Input MakeVar
-           , Input MakeCon
+           , Input MakeConSat
            ]
         <> mwhen (Map.member tInt tydefs) [Input MakeInt]
         <> mwhen (Map.member tChar tydefs) [Input MakeChar]
         <> mwhen
           (l /= Beginner)
           [ Input MakeVarSat
-          , Input MakeConSat
           , Input MakeLet
           , Input MakeLetRec
           , NoInput EnterHole
@@ -328,19 +326,11 @@ options ::
   -- or found but didn't correspond to the expected sort of entity (type/expr/pattern).
   Maybe Options
 options typeDefs defs cxt level def mNodeSel = \case
-  MakeCon ->
-    pure
-      . noFree
-      . map (globalOpt . valConName . snd)
-      . filter (not . (&& level == Beginner) . uncurry hasArgsCon)
-      . concatMap (\td -> (td,) <$> astTypeDefConstructors td)
-      . mapMaybe (typeDefAST . snd)
-      $ Map.toList typeDefs
   MakeConSat ->
     pure
       . noFree
       . map (globalOpt . valConName . snd)
-      . filter (uncurry hasArgsCon)
+      . filter (not . (&& level == Beginner) . uncurry hasArgsCon)
       . concatMap (\td -> (td,) <$> astTypeDefConstructors td)
       . mapMaybe (typeDefAST . snd)
       $ Map.toList typeDefs
@@ -461,7 +451,6 @@ sortByPriority l =
         DuplicateDef -> P.duplicate
         DeleteDef -> P.delete
       Input a -> case a of
-        MakeCon -> P.useValueCon
         MakeConSat -> P.useSaturatedValueCon
         MakeInt -> P.makeInt
         MakeChar -> P.makeChar

primer/src/Primer/Action/Priorities.hs

@@ -31,7 +31,6 @@
 module Primer.Action.Priorities (
   makeLambda,
   useVar,
-  useValueCon,
   makeInt,
   makeChar,
   makeCase,
@@ -73,9 +72,6 @@ makeLambda _ = 5
 useVar :: Level -> Int
 useVar _ = 10
 
-useValueCon :: Level -> Int
-useValueCon _ = 11
-
 makeCase :: Level -> Int
 makeCase _ = 12
 

primer/src/Primer/App.hs

@@ -64,7 +64,7 @@ import Control.Monad.Fresh (MonadFresh (..))
 import Control.Monad.Log (MonadLog, WithSeverity)
 import Control.Monad.NestedError (MonadNestedError, throwError')
 import Data.Data (Data)
-import Data.Generics.Uniplate.Operations (descendM, transform, transformM)
+import Data.Generics.Uniplate.Operations (transform, transformM)
 import Data.Generics.Uniplate.Zipper (
   fromZipper,
  )
@@ -144,7 +144,7 @@ import Primer.Core (
  )
 import Primer.Core.DSL (S, ann, create, emptyHole, hole, tEmptyHole, tvar)
 import Primer.Core.DSL qualified as DSL
-import Primer.Core.Transform (foldApp, renameVar, unfoldAPP, unfoldApp, unfoldTApp)
+import Primer.Core.Transform (renameVar, unfoldTApp)
 import Primer.Core.Utils (freeVars, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy)
 import Primer.Def (
   ASTDef (..),
@@ -772,7 +772,7 @@ applyProgAction prog mdefName = \case
           )
           type_
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons)
-      updateCons e =
+      updateCons =
         let typecache = _typecache % _Just
             -- Previously the @index@th argument @t@ to this
             -- constructor would have been typechecked against the old
@@ -798,25 +798,12 @@ applyProgAction prog mdefName = \case
               (_, Nothing, Just c) -> hole $ pure x `ann` generateTypeIDs c
               -- This last case means that the input program had no (useful) metadata
               (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole
-         in case (e, unfoldApp e) of
-              (Con m con' tys tms, _) | con' == con -> do
+         in transformM $ \case
+              Con m con' tys tms | con' == con -> do
                 adjustAtA index enhole tms >>= \case
-                  Just args' -> Con m con' tys <$> traverse (descendM updateCons) args'
+                  Just args' -> pure $ Con m con' tys args'
                   Nothing -> throwError $ ConNotSaturated con
-              -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced
-              -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments)
-              (_, (h, args)) -> case unfoldAPP h of
-                (Con _ con' [] [], _tyArgs) | con' == con -> do
-                  adjustAtA index enhole args >>= \case
-                    Just args' -> foldApp h =<< traverse (descendM updateCons) args'
-                    Nothing -> do
-                      -- The constructor is not applied as far as the changed field,
-                      -- so the full application still typechecks, but its type has changed.
-                      -- Thus, we put the whole thing in to a hole.
-                      Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
-                _ ->
-                  -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
-                  descendM updateCons e
+              e -> pure e
       updateDecons = transformCaseBranches prog type_ $
         traverse $ \cb@(CaseBranch vc binds e) ->
           if vc == con
@@ -858,27 +845,13 @@ applyProgAction prog mdefName = \case
       -- synthesis of the scrutinee's type, using the old typedef. Thus we must
       -- not update the scrutinee before this happens.
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
-      updateCons e = case (e, unfoldApp e) of
-        (Con m con' tys tms, _) | con' == con -> do
+      updateCons = transformM $ \case
+        Con m con' tys tms | con' == con -> do
           m' <- DSL.meta
           case insertAt index (EmptyHole m') tms of
-            Just args' -> Con m con' tys <$> traverse (descendM updateCons) args'
+            Just args' -> pure $ Con m con' tys args'
             Nothing -> throwError $ ConNotSaturated con
-        -- TODO (saturated constructors) this deconstruction of application nodes can be removed once full-saturation is enforced
-        -- (it currently assumes that constructors will either be fully saturated or have no syntactic arguments)
-        (_, (h, args)) -> case unfoldAPP h of
-          (Con _ con' [] [], _tyArgs) | con' == con -> do
-            m' <- DSL.meta
-            case insertAt index (EmptyHole m') args of
-              Just args' -> foldApp h =<< traverse (descendM updateCons) args'
-              Nothing ->
-                -- The constructor is not applied as far as the field immediately prior to the new one,
-                -- so the full application still typechecks, but its type has changed.
-                -- Thus, we put the whole thing in to a hole.
-                Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
-          _ ->
-            -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
-            descendM updateCons e
+        e -> pure e
       updateDecons = transformCaseBranches prog type_ $
         traverse $ \cb@(CaseBranch vc binds e) ->
           if vc == con

primer/src/Primer/Core.hs

@@ -224,6 +224,7 @@ data Expr' a b
 -- become synthesisable.
 
 -- Note [Synthesisable constructors]
+--
 -- Whilst our calculus is heavily inspired by bidirectional type systems
 -- (especially McBride's principled rendition), we do not treat constructors
 -- in this fashion. However, we are in the middle of changing the treatment
@@ -236,30 +237,36 @@ data Expr' a b
 -- changed, due to asymmetries between construction and matching.)
 --
 -- We represent a constructor-applied-to-a-spine as a thing (and one can infer
--- its type), but do not insist that it is fully saturated.
--- Thus one has `Cons` is a term, and we can derive the synthesis
--- judgement `Cons ∈ ∀a. a -> List a -> List a`, but also that `Cons @a`,
--- `Cons @a x` and `Cons @a x y` are terms (for type `a` and terms `x, y`), with
--- the obvious synthesised types. This is a temporary situation, and we aim to
--- enforce full saturation (and no type applications) in due course.
+-- its type), where we insist that it is fully saturated.
+-- Thus whilst `Cons` is a term, it is ill-typed. The only well-formed
+-- `Cons` usages are `Cons @A x xs`, which synthesises `List A`
+-- when `A ∋ x` and `List A ∋ xs`.
+--
+-- Whilst this may be a bit inconsistent with the treatment of
+-- functions, it has the advantage of symmetry with construction and
+-- matching. (I.e. every time one sees a particular constructor, it
+-- has the same form: a head of that constructor, and the same number
+-- of (term) fields.)
+-- TODO (saturated constructors): technically, a construction will
+-- have type arguments/indices and a match will not, but this is
+-- temporary, as we will soon remove indices (which will require
+-- constructors to be only checkable, rather than synthesisable).
 --
--- For comparison, the bidirectional view would be that constructors must
--- always be fully applied, and one can only subject them to a typechecking
--- judgement where the type is an input.
--- Thus `List Int ∋ Cons 2 Nil`, but `Cons` and `Cons 2` are ill-typed.
--- Under this view, one needs to be aware of the difference between, say,
+-- Thus one needs to be aware of the difference between, say,
 -- a globally-defined function, and a constructor "of the same type".
 -- For example, one can partially apply an addition function and map it
 -- across a list: `map (1 +) [2,3]` is well-typed, but one cannot map
 -- the `Succ` constructor in the same way.
--- (Notice, however, that since one will always know what type one is
--- considering, the constructor does not need any type applications
--- corresponding to the parameters of its datatype.)
 -- Clearly one could eta-expand, (and if necessary add an annotation) to
 -- use as constructor non-saturatedly: e.g. write `map (λn . Succ n) [2,3]`.
 --
--- In effect, we just bake (various stages of) this translation into the core.
--- To do this, we require constructor names to be unique across different types.
+-- For comparison, the bidirectional view would be that constructors
+-- must always be fully applied (which is the same as our treatment),
+-- and one can only subject them to a typechecking judgement where the
+-- type is an input (which is different to our treatment), and they do
+-- not need to store their indices/type applications (different to our
+-- treatment).
+-- Thus `List Int ∋ Cons 2 Nil`, but `Cons 2 Nil` does not synthesise a type.
 
 -- Note [Case]
 -- We use a list for compatibility and ease of JSON