Start implementing dependent pairs that pack and unpack themselves au…

…tomatically.

Still to do:
  * Make sure unpacking happens after function application. It currently
    happens inside `instantiateSigma` which should be called after function
    application but currently isn't. Possibly a recent regression with the n-ary
    functions patch.
  * Allow more than one implicit argument to dependent pairs, distinguished by
    name.
  * Allow explicit packing and unpacking via named components.
  * Fix the hack where we special-case `UDecl` in `checkSigma`.
  * Deprecate the old explicit dependent pair, and perhaps even rule out
    dependency in data constructors.
  * Possibly replace some uses of `List` in the standard library with implicit
    dependent pairs.

Co-authored-by: Alexey Radul <[email protected]>

misc/dex.el

@@ -5,12 +5,18 @@
 ;; https://developers.google.com/open-source/licenses/bsd
 
 (setq dex-highlights
-  '(("--\\([^o].*$\\|$\\)"   . font-lock-comment-face)
+  `(("--\\([^o].*$\\|$\\)"   . font-lock-comment-face)
     ("^> .*$"                . font-lock-comment-face)
     ("^'\\(.\\|\n.\\)*\n\n"  . font-lock-comment-face)
     ("\\w+:"                 . font-lock-comment-face)
     ("^:\\w*"                . font-lock-preprocessor-face)
-    ("\\bdef\\b\\|\\bfor\\b\\|\\brof\\b\\|\\bcase\\b\\|\\bstruct\\b\\|\\bdata\\b\\|\\bwhere\\b\\|\\bof\\b\\|\\bif\\b\\|\\bthen\\b\\|\\belse\\b\\|\\binterface\\b\\|\\binstance\\b\\|\\bgiven\\b\\|\\bdo\\b\\|\\bview\\b\\|\\bimport\\b\\|\\bforeign\\b\\|\\bsatisfying\\b\\|\\bself\\b" .
+    (,(concat
+       "\\bdef\\b\\|\\bfor\\b\\|\\brof\\b\\|\\bcase\\b\\|"
+       "\\bstruct\\b\\|\\bdata\\b\\|\\bwhere\\b\\|\\bof\\b\\|"
+       "\\bif\\b\\|\\bthen\\b\\|\\belse\\b\\|\\binterface\\b\\|"
+       "\\binstance\\b\\|\\bgiven\\b\\|\\bdo\\b\\|\\bview\\b\\|"
+       "\\bwith\\b\\|\\bself\\b\\|"
+       "\\bimport\\b\\|\\bforeign\\b\\|\\bsatisfying\\b") .
            font-lock-keyword-face)
     ("--o"                               . font-lock-variable-name-face)
     ("[-.,!;$^&*:~+/=<>|?\\\\]"           . font-lock-variable-name-face)

src/lib/AbstractSyntax.hs

@@ -463,7 +463,7 @@ expr = propagateSrcE expr' where
       EvalBinOp s -> evalOp s
       DepAmpersand  -> do
         lhs' <- tyOptPat lhs
-        UDepPairTy . (UDepPairType lhs') <$> expr rhs
+        UDepPairTy . (UDepPairType ExplicitDepPair lhs') <$> expr rhs
       DepComma      -> UDepPair <$> (expr lhs) <*> expr rhs
       CSEqual       -> throw SyntaxErr "Equal sign must be used as a separator for labels or binders, not a standalone operator"
       Colon         -> throw SyntaxErr "Colon separates binders from their type annotations, is not a standalone operator.\nIf you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)"
@@ -534,6 +534,13 @@ expr = propagateSrcE expr' where
     return $ UCase p'
       [ UAlt (nsB $ UPatCon "True"  Empty) c'
       , UAlt (nsB $ UPatCon "False" Empty) a']
+  expr' (CWith lhs rhs) = do
+    ty <- expr lhs
+    case rhs of
+      [b] -> do
+        b' <- binderOptTy b
+        return $ UDepPairTy $ UDepPairType ImplicitDepPair b' ty
+      _ -> error "n-ary dependent pairs not implemented"
 
 charExpr :: Char -> (UExpr' VoidS)
 charExpr c = UPrim (UPrimCon $ Lit $ Word8Lit $ fromIntegral $ fromEnum c) []

src/lib/Builder.hs

@@ -1397,14 +1397,14 @@ buildTelescopeVal xsTop tyTop = fst <$> go tyTop xsTop where
       (x1, ~(xDep : rest')) <- go ty1 rest
       ty2' <- applySubst (b@>SubstVal xDep) ty2
       (x2, rest'') <- go ty2' rest'
-      let depPairTy = DepPairType b (telescopeTypeType ty2)
+      let depPairTy = DepPairType ExplicitDepPair b (telescopeTypeType ty2)
       return (PairVal x1 (DepPair xDep x2 depPairTy), rest'')
 
 telescopeTypeType :: TelescopeType (AtomNameC r) (Type r) n -> Type r n
 telescopeTypeType (ProdTelescope tys) = ProdTy tys
 telescopeTypeType (DepTelescope lhs (Abs b rhs)) = do
   let lhs' = telescopeTypeType lhs
-  let rhs' = DepPairTy (DepPairType b (telescopeTypeType rhs))
+  let rhs' = DepPairTy (DepPairType ExplicitDepPair b (telescopeTypeType rhs))
   PairTy lhs' rhs'
 
 unpackTelescope

src/lib/CheapReduction.hs

@@ -386,7 +386,7 @@ liftSimpAtom ty simpAtom = case simpAtom of
       (BaseTy _  , Con (Lit v))      -> return $ Con $ Lit v
       (ProdTy tys, Con (ProdCon xs))   -> Con . ProdCon <$> zipWithM rec tys xs
       (SumTy  tys, Con (SumCon _ i x)) -> Con . SumCon tys i <$> rec (tys!!i) x
-      (DepPairTy dpt@(DepPairType (b:>t1) t2), DepPair x1 x2 _) -> do
+      (DepPairTy dpt@(DepPairType _ (b:>t1) t2), DepPair x1 x2 _) -> do
         x1' <- rec t1 x1
         t2' <- applySubst (b@>SubstVal x1') t2
         x2' <- rec t2' x2
@@ -414,7 +414,7 @@ confuseGHC = getDistinct
 -- CheapReduction and QueryType import?
 
 depPairLeftTy :: DepPairType r n -> Type r n
-depPairLeftTy (DepPairType (_:>ty) _) = ty
+depPairLeftTy (DepPairType _ (_:>ty) _) = ty
 {-# INLINE depPairLeftTy #-}
 
 unwrapNewtypeType :: EnvReader m => NewtypeTyCon n -> m n (NewtypeCon n, Type CoreIR n)
@@ -467,7 +467,7 @@ makeStructRepVal tyConName args = do
     _ -> return $ ProdVal args
 
 instantiateDepPairTy :: (IRRep r, EnvReader m) => DepPairType r n -> Atom r n -> m n (Type r n)
-instantiateDepPairTy (DepPairType b rhsTy) x = applyAbs (Abs b rhsTy) (SubstVal x)
+instantiateDepPairTy (DepPairType _ b rhsTy) x = applyAbs (Abs b rhsTy) (SubstVal x)
 {-# INLINE instantiateDepPairTy #-}
 
 projType :: (IRRep r, EnvReader m) => Int -> Type r n -> Atom r n -> m n (Type r n)

src/lib/CheckType.hs

@@ -339,7 +339,7 @@ instance HasType CoreIR DictExpr where
   getTypeE e = dictExprType e
 
 instance IRRep r => HasType r (DepPairType r) where
-  getTypeE (DepPairType b ty) = do
+  getTypeE (DepPairType _ b ty) = do
     checkB b \_ -> ty |: TyKind
     return TyKind
 
@@ -1074,7 +1074,7 @@ checkDataLike ty = case ty of
   TabPi (TabPiType b eltTy) -> do
     renameBinders b \_ ->
       checkDataLike eltTy
-  DepPairTy (DepPairType b@(_:>l) r) -> do
+  DepPairTy (DepPairType _ b@(_:>l) r) -> do
     recur l
     renameBinders b \_ -> checkDataLike r
   NewtypeTyCon LabelType -> notData

src/lib/ConcreteSyntax.hs

@@ -439,6 +439,9 @@ givenClause = keyWord GivenKW >> do
   (,) <$> parens (commaSep cGroup)
       <*> optional (parens (commaSep cGroup))
 
+withClause :: Parser WithClause
+withClause = keyWord WithKW >> parens (commaSep cGroup)
+
 arrowOptEffs :: Parser (Maybe CEffs)
 arrowOptEffs = sym "->" >> optional cEffs
 
@@ -704,6 +707,7 @@ ops =
   , [symOpR   ":"]
   , [symOpR  ",>"]
   , [symOpR  "&>"]
+  , [withClausePostfix]
   , [symOpL   "="]
   ] where
   other = ("other", anySymOp)
@@ -760,6 +764,13 @@ binApp :: Bin' -> SrcPos -> Group -> Group -> Group
 binApp f pos x y = joinSrc3 f' x y $ CBin f' x y
   where f' = WithSrc (Just pos) f
 
+withClausePostfix :: (SourceName, Expr.Operator Parser Group)
+withClausePostfix = ("with", op)
+  where
+    op = Expr.Postfix do
+      rhs <- withClause
+      return \lhs -> WithSrc Nothing $ CWith lhs rhs  -- TODO: source info
+
 withSrc :: Parser a -> Parser (WithSrc a)
 withSrc p = do
   (x, pos) <- withPos p

src/lib/GenericTraversal.hs

@@ -170,10 +170,10 @@ instance GenericallyTraversableE CoreIR TyConParams where
     TyConParams infs <$> mapM tge params
 
 instance IRRep r => GenericallyTraversableE r (DepPairType r) where
-  traverseGenericE (DepPairType (b:>lty) rty) = do
+  traverseGenericE (DepPairType expl (b:>lty) rty) = do
     lty' <- tge lty
     withFreshBinder (getNameHint b) lty' \b' -> do
-      extendRenamer (b@>binderName b') $ DepPairType b' <$> tge rty
+      extendRenamer (b@>binderName b') $ DepPairType expl b' <$> tge rty
 
 instance IRRep r => GenericallyTraversableE r (BaseMonoid r) where
   traverseGenericE (BaseMonoid x f) = BaseMonoid <$> tge x <*> tge f

src/lib/Imp.hs

@@ -710,7 +710,7 @@ typeToTree tyTop = return $ go REmpty tyTop
     BaseTy b -> Leaf $ LeafType (unRNest ctx) b
     TabTy b bodyTy -> go (RNest ctx (TabCtx b)) bodyTy
     RefTy _ t -> go (RNest ctx RefCtx) t
-    DepPairTy (DepPairType (b:>t1) (t2)) -> do
+    DepPairTy (DepPairType _ (b:>t1) (t2)) -> do
       let tree1 = rec t1
       let tree2 = go (RNest ctx (DepPairCtx (JustB (b:>t1)))) t2
       Branch [tree1, tree2]
@@ -746,7 +746,7 @@ valueToTree (RepVal tyTop valTop) = do
     BaseTy b -> return $ Leaf $ LeafType (unRNest ctx) b
     TabTy b bodyTy -> go (RNest ctx (TabCtx b)) bodyTy val
     RefTy _ t -> go (RNest ctx RefCtx) t val
-    DepPairTy (DepPairType (b:>t1) (t2)) -> case val of
+    DepPairTy (DepPairType _ (b:>t1) (t2)) -> case val of
       Branch [v1, v2] -> do
         case ctx of
           REmpty -> do

src/lib/Inference.hs

@@ -705,8 +705,8 @@ hoistInfStateRec env emissions !infVars defaults !subst decls e = case emissions
           -- If a variable is solved, we eliminate it.
           Just bSolutionUnhoisted -> do
             bSolution <-
-              liftHoistExcept' "Failed to eliminate solved variable in hoistInfStateRec"
-              $ hoist frag bSolutionUnhoisted
+              liftHoistExcept' "Failed to eliminate solved variable in hoistInfStateRec "
+                $ hoist frag bSolutionUnhoisted
             case exchangeBs $ PairB b infVars of
               -- This used to be accepted by the code at some point (and handled the same way
               -- as the Nothing) branch above, but I don't understand why. We don't even seem
@@ -850,6 +850,15 @@ checkSigma hint expr sTy = confuseGHC >>= \_ -> case sTy of
             _ -> Nothing
           expr' <- inferWithoutInstantiation expr >>= zonk
           dropSubst $ checkOrInferApp expr' explicits [] (Check resultTy)
+  DepPairTy depPairTy -> case depPairTy of
+    DepPairType ImplicitDepPair (_ :> lhsTy) _ -> do
+      -- TODO: check for the case that we're given some of the implicit dependent pair args explicitly
+      lhsVal <- Var <$> freshInferenceName MiscInfVar lhsTy
+      -- TODO: make an InfVarDesc case for dep pair instantiation
+      rhsTy <- instantiateDepPairTy depPairTy lhsVal
+      rhsVal <- checkSigma noHint expr rhsTy
+      return $ DepPair lhsVal rhsVal depPairTy
+    _ -> fallback
   _ -> fallback
   where fallback = checkOrInferRho hint expr (Check sTy)
 
@@ -898,6 +907,8 @@ withUDecl (WithSrcB src d) cont = addSrcContext src case d of
     var <- emitDecl (getNameHint p) letAnn $ Atom val
     bindLetPat p var cont
 
+-- "rho" means the required type here should not be (at the top level) an implicit pi type or
+-- an implicit dependent pair type. We don't want to unify those directly.
 -- The name hint names the object being computed
 checkOrInferRho
   :: forall i o. EmitsBoth o
@@ -939,16 +950,16 @@ checkOrInferRho hint uExprWithSrc@(WithSrcE pos expr) reqTy = do
         let msg =  "Can't reduce type expression: " ++ docAsStr (pretty ty)
         withReducibleEmissions msg $ checkUType ty
     matchRequirement $ TabPi piTy
-  UDepPairTy (UDepPairType (UAnnBinder b ann cs) rhs) -> do
+  UDepPairTy (UDepPairType expl (UAnnBinder b ann cs) rhs) -> do
     unless (null cs) $ throw TypeErr "Dependent pair binders shouldn't have constraints"
     ann' <- checkAnn (getSourceName b) ann
     matchRequirement =<< liftM DepPairTy do
-      buildDepPairTyInf (getNameHint b) ann' \v -> extendRenamer (b@>v) do
+      buildDepPairTyInf (getNameHint b) expl ann' \v -> extendRenamer (b@>v) do
         let msg =  "Can't reduce type expression: " ++ docAsStr (pretty rhs)
         withReducibleEmissions msg $ checkUType rhs
   UDepPair lhs rhs -> do
     case reqTy of
-      Check (DepPairTy ty@(DepPairType (_ :> lhsTy) _)) -> do
+      Check (DepPairTy ty@(DepPairType _ (_ :> lhsTy) _)) -> do
         lhs' <- checkSigmaDependent noHint lhs lhsTy
         rhsTy <- instantiateDepPairTy ty lhs'
         rhs' <- checkSigma noHint rhs rhsTy
@@ -1178,13 +1189,19 @@ instantiateSigma sigmaAtom = getType sigmaAtom >>= \case
   Pi (CorePiType ImplicitApp bs _ resultTy) -> do
     args <- inferMixedArgs @UExpr fDesc (Abs bs resultTy) [] []
     applySigmaAtom sigmaAtom args
-  _ -> case sigmaAtom of
-    SigmaAtom _ x -> return x
-    SigmaUVar _ v -> case v of
-      UAtomVar v' -> return $ Var v'
-      _ -> applySigmaAtom sigmaAtom []
-    SigmaPartialApp _ _ -> error "shouldn't hit this case because we should have a pi type here"
- where
+  DepPairTy (DepPairType ImplicitDepPair _ _) ->
+    -- TODO: we should probably call instantiateSigma again here in case
+    -- we have nested dependent pairs. Also, it looks like this doesn't
+    -- get called after function application. We probably want to fix that.
+    fallback >>= getSnd
+  _ -> fallback
+  where
+   fallback = case sigmaAtom of
+     SigmaAtom _ x -> return x
+     SigmaUVar _ v -> case v of
+       UAtomVar v' -> return $ Var v'
+       _ -> applySigmaAtom sigmaAtom []
+     SigmaPartialApp _ _ -> error "shouldn't hit this case because we should have a pi type here"
    fDesc :: SourceName
    fDesc = getSourceName sigmaAtom
 
@@ -1388,7 +1405,7 @@ applyDataCon tc conIx topArgs = do
         where
           nargs = length args; ntys = length tys
           (curArgs, remArgs) = splitAt (ntys - 1) args
-      DepPairTy dpt@(DepPairType b rty') -> do
+      DepPairTy dpt@(DepPairType _ b rty') -> do
         rty'' <- applySubst (b@>SubstVal h) rty'
         ans <- wrap rty'' t
         return $ DepPair h ans dpt
@@ -1744,7 +1761,7 @@ dataConRepTy (Abs topBs UnitE) = case topBs of
             (tailTy, tailIdxs) = go [] (ProjectProduct 1 : (depTyIdxs ++ projIdxs)) bs
             idxs = (iota accSize <&> \i -> ProjectProduct i : projIdxs) ++
                    ((ProjectProduct 0 : (depTyIdxs ++ projIdxs)) : tailIdxs)
-            depTy = DepPairTy $ DepPairType b tailTy
+            depTy = DepPairTy $ DepPairType ExplicitDepPair b tailTy
 
 inferClassDef
   :: EmitsInf o
@@ -3075,7 +3092,7 @@ synthDictForData dictTy@(DictType "Data" dName [ty]) = case ty of
   -- The "Var" case is different
   Var _ -> synthDictFromGiven dictTy
   TabPi (TabPiType b eltTy) -> recurBinder (Abs b eltTy) >> success
-  DepPairTy (DepPairType b@(_:>l) r) -> do
+  DepPairTy (DepPairType _ b@(_:>l) r) -> do
     recur l >> recurBinder (Abs b r) >> success
   NewtypeTyCon LabelType -> notData
   NewtypeTyCon nt -> do
@@ -3219,12 +3236,12 @@ buildTabPiInf hint ixTy body = do
 
 buildDepPairTyInf
   :: EmitsInf n
-  => NameHint -> CType n
+  => NameHint -> DepPairExplicitness -> CType n
   -> (forall l. (EmitsInf l, Ext n l) => CAtomName l -> InfererM i l (CType l))
   -> InfererM i n (DepPairType CoreIR n)
-buildDepPairTyInf hint ty body = do
+buildDepPairTyInf hint expl ty body = do
   Abs b resultTy <- buildAbsInf hint Explicit ty body
-  return $ DepPairType (withoutExpl b) resultTy
+  return $ DepPairType expl (withoutExpl b) resultTy
 
 buildAltInf
   :: EmitsInf n

src/lib/Lexing.hs

@@ -80,7 +80,7 @@ checkNotKeyword p = try $ do
 
 data KeyWord = DefKW | ForKW | For_KW | RofKW | Rof_KW | CaseKW | OfKW
              | DataKW | StructKW | InterfaceKW
-             | InstanceKW | GivenKW | SatisfyingKW
+             | InstanceKW | GivenKW | WithKW | SatisfyingKW
              | IfKW | ThenKW | ElseKW | DoKW
              | ImportKW | ForeignKW | NamedInstanceKW
              | EffectKW | HandlerKW | JmpKW | CtlKW | ReturnKW | ResumeKW
@@ -105,6 +105,7 @@ keyWordToken = \case
   InstanceKW      -> "instance"
   NamedInstanceKW -> "named-instance"
   GivenKW         -> "given"
+  WithKW          -> "with"
   SatisfyingKW    -> "satisfying"
   DoKW            -> "do"
   ImportKW        -> "import"

src/lib/PPrint.hs

@@ -259,7 +259,7 @@ instance Pretty (DictType n) where
 
 instance IRRep r => Pretty (DepPairType r n) where pretty = prettyFromPrettyPrec
 instance IRRep r => PrettyPrec (DepPairType r n) where
-  prettyPrec (DepPairType b rhs) =
+  prettyPrec (DepPairType _ b rhs) =
     atPrec ArgPrec $ align $ group $ parens $ p b <+> "&>" <+> p rhs
 
 instance Pretty (EffectOpType n) where
@@ -656,7 +656,8 @@ instance PrettyPrec (UTabPiExpr n) where
 
 instance Pretty (UDepPairType n) where pretty = prettyFromPrettyPrec
 instance PrettyPrec (UDepPairType n) where
-  prettyPrec (UDepPairType pat ty) = atPrec LowestPrec $ align $
+  -- TODO: print explicitness info
+  prettyPrec (UDepPairType _ pat ty) = atPrec LowestPrec $ align $
     p pat <+> "&>" <+> pLowest ty
 
 instance Pretty (UBlock' n) where

src/lib/QueryType.hs

@@ -755,7 +755,7 @@ rawStrType :: IRRep r => EnvReader m => m n (Type r n)
 rawStrType = liftEnvReaderM do
   withFreshBinder "n" IdxRepTy \b -> do
     tabTy <- rawFinTabType (Var $ binderName b) CharRepTy
-    return $ DepPairTy $ DepPairType b tabTy
+    return $ DepPairTy $ DepPairType ExplicitDepPair b tabTy
 
 -- `n` argument is IdxRepVal, not Nat
 rawFinTabType :: IRRep r => EnvReader m => Atom r n -> Atom r n -> m n (Type r n)

src/lib/Simplify.hs

@@ -143,12 +143,12 @@ getRepType ty = go ty where
       RefType h a -> RefType  <$> toDataAtomIgnoreReconAssumeNoDecls h <*> go a
       TypeKind    -> error $ notDataType
       HeapType    -> return $ HeapType
-    DepPairTy (DepPairType b@(_:>l) r) -> do
+    DepPairTy (DepPairType expl b@(_:>l) r) -> do
       l' <- go l
       withFreshBinder (getNameHint b) l' \b' -> do
         x <- liftSimpAtom (sink l) (Var $ binderName b')
         r' <- go =<< applySubst (b@>SubstVal x) r
-        return $ DepPairTy $ DepPairType b' r'
+        return $ DepPairTy $ DepPairType expl b' r'
     TabPi (TabPiType (b:>ixTy) bodyTy) -> do
       ixTy' <- simplifyIxType ixTy
       withFreshBinder (getNameHint b) ixTy' \b' -> do

src/lib/SourceRename.hs

@@ -188,9 +188,9 @@ instance SourceRenamableE UExpr' where
     UTabPi (UTabPiExpr pat body) ->
       sourceRenameB pat \pat' ->
         UTabPi <$> (UTabPiExpr pat' <$> sourceRenameE body)
-    UDepPairTy (UDepPairType pat body) ->
+    UDepPairTy (UDepPairType expl pat body) ->
       sourceRenameB pat \pat' ->
-        UDepPairTy <$> (UDepPairType pat' <$> sourceRenameE body)
+        UDepPairTy <$> (UDepPairType expl pat' <$> sourceRenameE body)
     UDepPair lhs rhs ->
       UDepPair <$> sourceRenameE lhs <*> sourceRenameE rhs
     UTabApp f x -> UTabApp <$> sourceRenameE f <*> mapM sourceRenameE x

src/lib/Types/Core.hs

@@ -243,7 +243,7 @@ data CorePiType (n::S) where
   CorePiType :: AppExplicitness -> CoreBinders n l -> EffectRow CoreIR l -> Type CoreIR l -> CorePiType n
 
 data DepPairType (r::IR) (n::S) where
-  DepPairType :: Binder r n l -> Type r l -> DepPairType r n
+  DepPairType :: DepPairExplicitness -> Binder r n l -> Type r l -> DepPairType r n
 
 data Projection =
    UnwrapNewtype -- TODO: add `HasCore r` constraint
@@ -2009,10 +2009,10 @@ deriving via WrapE (PiType r) n instance IRRep r => Generic (PiType r n)
 instance IRRep r => Store (PiType r n)
 
 instance GenericE (DepPairType r) where
-  type RepE (DepPairType r) = Abs (Binder r) (Type r)
-  fromE (DepPairType b resultTy) = Abs b resultTy
+  type RepE (DepPairType r) = PairE (LiftE DepPairExplicitness) (Abs (Binder r) (Type r))
+  fromE (DepPairType expl b resultTy) = LiftE expl `PairE` Abs b resultTy
   {-# INLINE fromE #-}
-  toE   (Abs b resultTy) = DepPairType b resultTy
+  toE   (LiftE expl `PairE` Abs b resultTy) = DepPairType expl b resultTy
   {-# INLINE toE #-}
 
 instance IRRep r => SinkableE      (DepPairType r)