feat!: saturated constructors stage 5/5

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

@@ -105,10 +105,10 @@ genCon :: ExprGen Expr
 genCon =
   Gen.recursive
     Gen.choice
-    [genCon' (pure []) (pure [])]
-    [genCon' (Gen.list (Range.linear 0 3) genType) (Gen.list (Range.linear 0 5) genExpr)]
+    [genCon' (pure [])]
+    [genCon' (Gen.list (Range.linear 0 5) genExpr)]
   where
-    genCon' tys tms = Con <$> genMeta <*> genValConName <*> tys <*> tms
+    genCon' tms = Con <$> genMeta <*> genValConName <*> tms
 
 genLam :: ExprGen Expr
 genLam = Lam <$> genMeta <*> genLVarName <*> genExpr

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

@@ -87,7 +87,6 @@ import Primer.Typecheck (
   buildTypingContextFromModules',
   consistentKinds,
   consistentTypes,
-  decomposeTAppCon,
   extendLocalCxt,
   extendLocalCxtTy,
   extendLocalCxtTys,
@@ -387,7 +386,6 @@ genChk ty = do
               let cons' =
                     M.toList cons <&> \(c, (params, fldsTys0)) -> do
                       indicesMap <- for params $ \(p, k) -> (p,) <$> genWTType k
-                      let indices = snd <$> indicesMap
                       -- NB: it is vital to use simultaneous substitution here.
                       -- Consider the case where we have a local type variable @a@
                       -- in scope, say because we have already generated a
@@ -402,23 +400,16 @@ genChk ty = do
                       -- @Bool@.
                       fldsTys <- traverse (substTySimul $ M.fromList indicesMap) fldsTys0
                       flds <- traverse (Gen.small . genChk) fldsTys
-                      pure $ Con () c indices flds
+                      pure $ Con () c flds
               Gen.choice cons'
         Left _ -> pure Nothing -- not an ADT
         Right (_, _, []) -> pure Nothing -- is an empty ADT
-        -- TODO (saturated constructors) eventually (constructors are
-        -- saturated & checkable, and thus don't store their indices),
-        -- we will not need to record @params@ in the @Con@, and thus
-        -- the guard (and the panic) will be removed.
-        Right (tc, _, vcs)
-          | Just (tc', params) <- decomposeTAppCon ty
-          , tc == tc' ->
-              pure $
-                Just $
-                  Gen.choice $
-                    vcs <&> \(vc, tmArgTypes) ->
-                      Con () vc params <$> traverse genChk tmArgTypes
-          | otherwise -> panic "genCon invariants failed"
+        Right (_, _, vcs) ->
+          pure $
+            Just $
+              Gen.choice $
+                vcs <&> \(vc, tmArgTypes) ->
+                  Con () vc <$> traverse genChk tmArgTypes
     lambda =
       matchArrowType ty <&> \(sTy, tTy) -> do
         n <- genLVarNameAvoiding [tTy, sTy]

primer/src/Primer/API.hs

@@ -720,11 +720,11 @@ viewTreeExpr e0 = case e0 of
       , childTrees = [viewTreeExpr e, viewTreeType t]
       , rightChild = Nothing
       }
-  Con _ c tyApps tmApps ->
+  Con _ c tmApps ->
     Tree
       { nodeId
       , body = TextBody $ RecordPair Flavor.Con $ globalName c
-      , childTrees = map viewTreeType tyApps ++ map viewTreeExpr tmApps
+      , childTrees = map viewTreeExpr tmApps
       , rightChild = Nothing
       }
   Lam _ s e ->

primer/src/Primer/Action.hs

@@ -22,7 +22,6 @@ import Data.Aeson (Value)
 import Data.Bifunctor.Swap qualified as Swap
 import Data.Generics.Product (typed)
 import Data.List (findIndex)
-import Data.List.Extra ((!?))
 import Data.List.NonEmpty qualified as NE
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
@@ -130,7 +129,6 @@ import Primer.Zipper (
   findNodeWithParent,
   findType,
   focus,
-  focusConTypes,
   focusLoc,
   focusOn,
   focusType,
@@ -351,7 +349,6 @@ applyAction' a = case a of
   ConstructLAM x -> termAction (constructLAM x) "cannot construct function 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"
   ConstructLet x -> termAction (constructLet x) "cannot construct let in type"
   ConstructLetrec x -> termAction (constructLetrec x) "cannot construct letrec in type"
   ConvertLetToLetrec -> termAction convertLetToLetrec "cannot convert type to letrec"
@@ -365,12 +362,6 @@ applyAction' a = case a of
   ExitType -> \case
     InType zt -> pure $ InExpr $ unfocusType zt
     _ -> throwError $ CustomFailure ExitType "cannot exit type - not in type"
-  EnterConTypeArgument n -> \case
-    InExpr ze -> case (!? n) <$> focusConTypes ze of
-      Nothing -> throwError $ CustomFailure (EnterConTypeArgument n) "Move-to-constructor-argument failed: this is not a constructor"
-      Just Nothing -> throwError $ CustomFailure (EnterConTypeArgument n) "Move-to-constructor-argument failed: no such argument"
-      Just (Just z') -> pure $ InType z'
-    _ -> throwError $ CustomFailure (EnterConTypeArgument n) "cannot enter value constructors argument - not in expr"
   ConstructArrowL -> typeAction constructArrowL "cannot construct arrow - not in type"
   ConstructArrowR -> typeAction constructArrowR "cannot construct arrow - not in type"
   ConstructTCon c -> typeAction (constructTCon c) "cannot construct tcon in expr"
@@ -621,70 +612,34 @@ constructSatCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ
 constructSatCon c ze = case target ze of
   -- Similar comments re smartholes apply as to insertSatVar
   EmptyHole{} -> do
-    (_, nTyArgs, nTmArgs) <-
+    (_, nTmArgs) <-
       conInfo n >>= \case
         Left err -> throwError $ SaturatedApplicationError $ Left err
         Right t -> pure t
-    flip replace ze <$> con n (replicate nTyArgs tEmptyHole) (replicate nTmArgs emptyHole)
+    flip replace ze <$> con n (replicate nTmArgs emptyHole)
   e -> throwError $ NeedEmptyHole (ConstructSaturatedCon c) e
   where
     n = unsafeMkGlobalName c
 
 -- returns
 -- - "type" of ctor: the type an eta-expanded version of this constructor would check against
 --   e.g. @Cons@'s "type" is @∀a. a -> List a -> List a@.
--- - its arity (number of type args and number of term args required for full saturation)
+-- - its arity (number of args required for full saturation)
 conInfo ::
   MonadReader TC.Cxt m =>
   ValConName ->
-  m (Either Text (TC.Type, Int, Int))
+  m (Either Text (TC.Type, Int))
 conInfo c =
   asks (flip lookupConstructor c . TC.typeDefs) <&> \case
-    Just (vc, tc, td) -> Right (valConType tc td vc, length $ td.astTypeDefParameters, length $ vc.valConArgs)
+    Just (vc, tc, td) -> Right (valConType tc td vc, length $ vc.valConArgs)
     Nothing -> Left $ "Could not find constructor " <> show c
 
-constructRefinedCon :: ActionM m => QualifiedText -> ExprZ -> m ExprZ
-constructRefinedCon c ze = do
-  let n = unsafeMkGlobalName c
-  (cTy, numTyArgs, numTmArgs) <-
-    conInfo n >>= \case
-      Left err -> throwError $ RefineError $ Left err
-      Right t -> pure t
-  -- our Cxt in the monad does not care about the local context, we have to extract it from the zipper.
-  -- See https://github.com/hackworthltd/primer/issues/11
-  -- We only care about the type context for refine
-  let (tycxt, _) = localVariablesInScopeExpr (Left ze)
-  cxt <- asks $ TC.extendLocalCxtTys tycxt
-  tgtTy <- getTypeCache $ target ze
-  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) `ann` tEmptyHole)
-        -- See Note [No valid refinement]
-        -- NB: the inside of a hole must be synthesisable (see Note [Holes and bidirectionality])
-        Nothing -> flip replace ze <$> hole (con n (replicate numTyArgs tEmptyHole) (replicate numTmArgs emptyHole) `ann` tEmptyHole)
-        Just Nothing -> throwError $ InternalFailure "Types of constructors always have type abstractions before term abstractions"
-    e -> throwError $ NeedEmptyHole (ConstructRefinedCon c) e
-
 getTypeCache :: MonadError ActionError m => Expr -> m TypeCache
 getTypeCache =
   maybeTypeOf <&> \case
     Nothing -> throwError $ RefineError $ Left "Don't have a cached type"
     Just ty -> pure ty
 
--- | A view for lists where all 'Left' come before all 'Right'
-breakLR :: [Either a b] -> Maybe ([a], [b])
-breakLR =
-  spanMaybe leftToMaybe <&> \case
-    (ls, rest) -> (ls,) <$> traverse rightToMaybe rest
-
 constructLet :: ActionM m => Maybe Text -> ExprZ -> m ExprZ
 constructLet mx ze = case target ze of
   EmptyHole{} -> do
@@ -968,9 +923,8 @@ toProgActionInput ::
   Either ActionError [ProgAction]
 toProgActionInput def defName mNodeSel opt0 = \case
   Available.MakeConSat -> do
-    ref <- offerRefined
     opt <- optGlobal
-    toProg [if ref then ConstructRefinedCon opt else ConstructSaturatedCon opt]
+    toProg [ConstructSaturatedCon opt]
   Available.MakeInt -> do
     opt <- optNoCxt
     n <- maybeToEither (NeedInt opt0) $ readMaybe opt

primer/src/Primer/Action/Actions.hs

@@ -62,8 +62,6 @@ data Action
     ConstructPrim PrimCon
   | -- | Put a constructor applied to a saturated spine in an empty hole
     ConstructSaturatedCon QualifiedText
-  | -- | Put a constructor in an empty hole, and infer what it should be applied to
-    ConstructRefinedCon QualifiedText
   | -- | Put a let expression in an empty hole
     ConstructLet (Maybe Text)
   | -- | Put a letrec expression in an empty hole
@@ -80,17 +78,8 @@ data Action
     RenameLet Text
   | -- | Move from an annotation to its type
     EnterType
-  | -- TODO (saturated constructors) this includes moving from one of a
-    -- constructor's type arguments back to the constructor itself. This
-    -- will be removed when constructors no longer store their indices
-
-    -- | Move from a type up into the surrounding annotation
+  | -- | Move from a type up into the surrounding annotation
     ExitType
-  | -- TODO (saturated constructors) this is a temporary situation, and will be
-    -- removed once constructors no longer store their indices
-
-    -- | Move from a constructor into one if its type arguments (zero-indexed)
-    EnterConTypeArgument Int
   | -- | Construct a function type around the type under the cursor.
     -- The type under the cursor is placed in the domain (left) position.
     ConstructArrowL

primer/src/Primer/Action/Movement.hs

@@ -12,12 +12,6 @@ data Movement
   | Parent
   | Branch ValConName
   | -- | Move into a term argument of a saturated constructor (zero-indexed)
-    -- TODO (saturated constructors) the current, temporary, situation is that
-    -- constructors have both type arguments (indices) and term arguments. To move
-    -- into a term argument, one uses this @Movement@ type. To move into a *type*
-    -- argument, use the special 'EnterConTypeArgument' action (it cannot be a
-    -- movement because it changes from focusing on an expression to focusing on a
-    -- type).
     ConChild Int
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON Movement

primer/src/Primer/App.hs

@@ -799,9 +799,9 @@ applyProgAction prog mdefName = \case
               -- This last case means that the input program had no (useful) metadata
               (_, Nothing, Nothing) -> hole $ pure x `ann` tEmptyHole
          in transformM $ \case
-              Con m con' tys tms | con' == con -> do
+              Con m con' tms | con' == con -> do
                 adjustAtA index enhole tms >>= \case
-                  Just args' -> pure $ Con m con' tys args'
+                  Just args' -> pure $ Con m con' args'
                   Nothing -> throwError $ ConNotSaturated con
               e -> pure e
       updateDecons = transformCaseBranches prog type_ $
@@ -846,10 +846,10 @@ applyProgAction prog mdefName = \case
       -- not update the scrutinee before this happens.
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
       updateCons = transformM $ \case
-        Con m con' tys tms | con' == con -> do
+        Con m con' tms | con' == con -> do
           m' <- DSL.meta
           case insertAt index (EmptyHole m') tms of
-            Just args' -> pure $ Con m con' tys args'
+            Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
       updateDecons = transformCaseBranches prog type_ $

primer/src/Primer/Builtins/DSL.hs

@@ -29,7 +29,6 @@ import Primer.Builtins (
 import Primer.Core (
   Expr,
   ID,
-  TyConName,
   Type,
  )
 import Primer.Core.DSL (
@@ -53,21 +52,21 @@ nat = \case
   0 -> con0 cZero
   n -> con1 cSucc $ nat (n - 1)
 
-maybe_ :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr
-maybe_ t f = \case
-  Nothing -> con cNothing [t] []
-  Just x -> con cJust [t] [f x]
+maybe_ :: MonadFresh ID m => (a -> m Expr) -> Maybe a -> m Expr
+maybe_ f = \case
+  Nothing -> con cNothing []
+  Just x -> con cJust [f x]
 
 maybeAnn :: MonadFresh ID m => m Type -> (a -> m Expr) -> Maybe a -> m Expr
-maybeAnn t f x = maybe_ t f x `ann` (tcon tMaybe `tapp` t)
+maybeAnn t f x = maybe_ f x `ann` (tcon tMaybe `tapp` t)
 
-list_ :: MonadFresh ID m => TyConName -> [m Expr] -> m Expr
-list_ t =
+list_ :: MonadFresh ID m => [m Expr] -> m Expr
+list_ =
   foldr
     ( \a b ->
-        con cCons [tcon t] [a, b]
+        con cCons [a, b]
     )
-    (con cNil [tcon t] [])
+    (con cNil [])
 
 listOf :: MonadFresh ID m => m Type -> m Type
 listOf = tapp (tcon tList)

primer/src/Primer/Core.hs

@@ -34,12 +34,12 @@ import Data.Generics.Product
 import Data.Generics.Uniplate.Data ()
 import Optics (
   AffineFold,
+  AffineTraversal',
   Lens,
   Lens',
   Traversal,
-  Traversal',
   afailing,
-  traversalVL,
+  atraversalVL,
   (%),
  )
 import Primer.Core.Meta (
@@ -145,7 +145,7 @@ data Expr' a b
   | Ann a (Expr' a b) (Type' b)
   | App a (Expr' a b) (Expr' a b)
   | APP a (Expr' a b) (Type' b)
-  | Con a ValConName [Type' b] [Expr' a b] -- See Note [Checkable constructors]
+  | Con a ValConName [Expr' a b] -- See Note [Checkable constructors]
   | Lam a LVarName (Expr' a b)
   | LAM a TyVarName (Expr' a b)
   | Var a TmVarRef
@@ -232,23 +232,15 @@ data Expr' a b
 -- We represent a constructor-applied-to-a-spine as a thing (and can
 -- only check 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 checks against `List A`
+-- `Cons` usages are `Cons x xs`, which checks against `List A`
 -- when `A ∋ x` and `List A ∋ xs`.
---
--- TODO (saturated constructors): the occurence of `@A` above is a temporary
--- wart here, and will be removed in due course. (It was needed when
--- constructors were still synthesisable, but is now a needless
--- complication. It also leads to some inaccuracies in this
--- description of the typing rule.)
+-- (Note that there are no type arguments here!)
 --
 -- 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.
 --
 -- As an example, `List Int ∋ Cons 2 Nil`, but `Cons` and `Cons 2` are ill-typed.
 -- Thus one needs to be aware of the difference between, say,
@@ -261,10 +253,6 @@ data Expr' a b
 -- 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]`.
---
--- TODO (saturated constructors): the above parenthetical about not
--- needing type applications is not currently true, but will be
--- shortly.
 
 -- Note [Case]
 -- We use a list for compatibility and ease of JSON
@@ -326,16 +314,13 @@ _bindMeta :: forall a b. Lens (Bind' a) (Bind' b) a b
 _bindMeta = position @1
 
 -- | Note that this does not recurse in to sub-expressions or sub-types.
-typesInExpr :: Traversal' (Expr' a b) (Type' b)
--- TODO (saturated constructors): if constructors did not store their indices,
--- then this could be an affine traversal
-typesInExpr = traversalVL $ \f -> \case
+typesInExpr :: AffineTraversal' (Expr' a b) (Type' b)
+typesInExpr = atraversalVL $ \point f -> \case
   Ann m e ty -> Ann m e <$> f ty
   APP m e ty -> APP m e <$> f ty
-  Con m c tys tms -> Con m c <$> traverse f tys <*> pure tms
   LetType m x ty e -> (\ty' -> LetType m x ty' e) <$> f ty
   Letrec m x b ty e -> (\ty' -> Letrec m x b ty' e) <$> f ty
-  e -> pure e
+  e -> point e
 
 instance HasID a => HasID (Expr' a b) where
   _id = position @1 % _id