[ impl ] Support default implicits in named implementations (#3100)

CHANGELOG.md

@@ -20,6 +20,7 @@
 * New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`,
   `Name`, and `Decls` literals.
 * Call to `%macro`-functions do not require the `ElabReflection` extension.
+* Default implicits are supported for named implementations.
 * Elaborator scripts were made to be able to access project files,
   allowing the support for type providers and similar stuff.
 

src/Idris/Desugar.idr

@@ -911,6 +911,15 @@ mutual
       = do tms' <- traverse (desugar AnyExpr ps) tms
            pure (ForeignExport tms')
 
+  %inline
+  mapDesugarPiInfo : {auto s : Ref Syn SyntaxInfo} ->
+                     {auto c : Ref Ctxt Defs} ->
+                     {auto u : Ref UST UState} ->
+                     {auto m : Ref MD Metadata} ->
+                     {auto o : Ref ROpts REPLOpts} ->
+                     List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
+  mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps)
+
   -- Given a high level declaration, return a list of TTImp declarations
   -- which process it, and update any necessary state on the way.
   export
@@ -1019,9 +1028,10 @@ mutual
 
   desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body)
       = do opts <- traverse (desugarFnOpt ps) fnopts
-           is' <- for is $ \ (fc, c,n,tm) =>
+           is' <- for is $ \ (fc, c, n, pi, tm) =>
                      do tm' <- desugar AnyExpr ps tm
-                        pure (fc, c, n, tm')
+                        pi' <- mapDesugarPiInfo ps pi
+                        pure (fc, c, n, pi', tm')
            cons' <- for cons $ \ (n, tm) =>
                      do tm' <- desugar AnyExpr ps tm
                         pure (n, tm')
@@ -1034,13 +1044,13 @@ mutual
              $ findUniqueBindableNames fc True ps []
 
            let paramsb = map (doBind bnames) params'
-           let isb = map (\ (info, r, n, tm) => (info, r, n, doBind bnames tm)) is'
+           let isb = map (\ (info, r, n, p, tm) => (info, r, n, p, doBind bnames tm)) is'
            let consb = map (\(n, tm) => (n, doBind bnames tm)) cons'
 
            body' <- maybe (pure Nothing)
                           (\b => do b' <- traverse (desugarDecl ps) b
                                     pure (Just (concat b'))) body
-           -- calculate the name of the interface, if it's not explicitly
+           -- calculate the name of the implementation, if it's not explicitly
            -- given.
            let impname = maybe (mkImplName fc tn paramsb) id impln
 
@@ -1102,9 +1112,6 @@ mutual
           NS ns (DN str (MN ("__mk" ++ str) 0))
       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
 
-      mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
-      mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)
-
   desugarDecl ps (PFixity fc vis fix prec opName)
       = do ctx <- get Ctxt
            -- We update the context of fixities by adding a namespaced fixity

src/Idris/Elab/Implementation.idr

@@ -47,10 +47,10 @@ bindConstraints fc p [] ty = ty
 bindConstraints fc p ((n, ty) :: rest) sc
     = IPi fc top p n ty (bindConstraints fc p rest sc)
 
-bindImpls : List (FC, RigCount, Name, RawImp) -> RawImp -> RawImp
+bindImpls : List (FC, RigCount, Name, PiInfo RawImp, RawImp) -> RawImp -> RawImp
 bindImpls [] ty = ty
-bindImpls ((fc, r, n, ty) :: rest) sc
-    = IPi fc r Implicit (Just n) ty (bindImpls rest sc)
+bindImpls ((fc, r, n, p, ty) :: rest) sc
+    = IPi fc r p (Just n) ty (bindImpls rest sc)
 
 addDefaults : FC -> Name ->
               (params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
@@ -99,11 +99,16 @@ addDefaults fc impName params allms defs body
 getMethImps : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               Env Term vars -> Term vars ->
-              Core (List (Name, RigCount, RawImp))
+              Core (List (Name, RigCount, Maybe RawImp, RawImp))
 getMethImps env (Bind fc x (Pi fc' c Implicit ty) sc)
     = do rty <- map (map rawName) $ unelabNoSugar env ty
          ts <- getMethImps (Pi fc' c Implicit ty :: env) sc
-         pure ((x, c, rty) :: ts)
+         pure ((x, c, Nothing, rty) :: ts)
+getMethImps env (Bind fc x (Pi fc' c (DefImplicit def) ty) sc)
+    = do rty <- map (map rawName) $ unelabNoSugar env ty
+         rdef <- map (map rawName) $ unelabNoSugar env def
+         ts <- getMethImps (Pi fc' c (DefImplicit def) ty :: env) sc
+         pure ((x, c, Just rdef, rty) :: ts)
 getMethImps env tm = pure []
 
 export
@@ -115,7 +120,7 @@ elabImplementation : {vars : _} ->
                      {auto o : Ref ROpts REPLOpts} ->
                      FC -> Visibility -> List FnOpt -> Pass ->
                      Env Term vars -> NestedNames vars ->
-                     (implicits : List (FC, RigCount, Name, RawImp)) ->
+                     (implicits : List (FC, RigCount, Name, PiInfo RawImp, RawImp)) ->
                      (constraints : List (Maybe Name, RawImp)) ->
                      Name ->
                      (ps : List RawImp) ->
@@ -346,7 +351,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
     -- When applying the method in the field for the record, eta expand
     -- the expected arguments based on the field type, so that implicits get
     -- inserted in the right place
-    mkMethField : List (Name, RigCount, RawImp) ->
+    mkMethField : List (Name, a) ->
                   List (Name, List (Name, RigCount, PiInfo RawImp)) ->
                   (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp
     mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
@@ -378,16 +383,18 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
         = do mn <- inCurrentNS (methName n)
              pure (dropNS n, IVar vfc mn)
 
-    bindImps : List (Name, RigCount, RawImp) -> RawImp -> RawImp
+    bindImps : List (Name, RigCount, Maybe RawImp, RawImp) -> RawImp -> RawImp
     bindImps [] ty = ty
-    bindImps ((n, c, t) :: ts) ty
+    bindImps ((n, c, Just def, t) :: ts) ty
+        = IPi vfc c (DefImplicit def) (Just n) t (bindImps ts ty)
+    bindImps ((n, c, Nothing, t) :: ts) ty
         = IPi vfc c Implicit (Just n) t (bindImps ts ty)
 
     -- Return method name, specialised method name, implicit name updates,
     -- and method type. Also return how the method name should be updated
     -- in later method types (specifically, putting implicits in)
     topMethType : List (Name, RawImp) ->
-                  Name -> List (Name, RigCount, RawImp) ->
+                  Name -> List (Name, RigCount, Maybe RawImp, RawImp) ->
                   List String -> List Name -> List Name -> List Name ->
                   Method ->
                   Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
@@ -445,7 +452,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
              pure ((meth.name, n, upds, meth.count, meth.totalReq, mty), methupds')
 
     topMethTypes : List (Name, RawImp) ->
-                   Name -> List (Name, RigCount, RawImp) ->
+                   Name -> List (Name, RigCount, Maybe RawImp, RawImp) ->
                    List String ->
                    List Name -> List Name -> List Name ->
                    List Method ->

src/Idris/Parser.idr

@@ -1594,6 +1594,16 @@ recordConstructor fname
        n <- mustWork $ decoratedDataConstructorName fname
        pure (doc, n)
 
+autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t)
+autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto"
+
+defImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo PTerm)
+defImplicitField fname indents = do
+  decoratedKeyword fname "default"
+  commit
+  t <- simpleExpr fname indents
+  pure (DefImplicit t)
+
 constraints : OriginDesc -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
 constraints fname indents
     = do tm <- appExpr pdef fname indents
@@ -1610,15 +1620,22 @@ constraints fname indents
          pure ((Just n, tm) :: more)
   <|> pure []
 
-implBinds : OriginDesc -> IndentInfo -> EmptyRule (List (FC, RigCount, Name, PTerm))
-implBinds fname indents = concatMap (map adjust) <$> go where
+implBinds : OriginDesc -> IndentInfo -> (namedImpl : Bool) -> EmptyRule (List (FC, RigCount, Name, PiInfo PTerm, PTerm))
+implBinds fname indents namedImpl = concatMap (map adjust) <$> go where
 
-  adjust : (RigCount, WithBounds Name, PTerm) -> (FC, RigCount, Name, PTerm)
+  adjust : (RigCount, WithBounds Name, a) -> (FC, RigCount, Name, a)
   adjust (r, wn, ty) = (virtualiseFC (boundToFC fname wn), r, wn.val, ty)
 
-  go : EmptyRule (List (List (RigCount, WithBounds Name, PTerm)))
+  isDefaultImplicit : PiInfo a -> Bool
+  isDefaultImplicit (DefImplicit _) = True
+  isDefaultImplicit _               = False
+
+  go : EmptyRule (List (List (RigCount, WithBounds Name, PiInfo PTerm, PTerm)))
   go = do decoratedSymbol fname "{"
-          ns <- pibindListName fname indents
+          piInfo <- bounds $ option Implicit $ defImplicitField fname indents
+          when (not namedImpl && isDefaultImplicit piInfo.val) $
+            fatalLoc piInfo.bounds "Default implicits are allowed only for named implementations"
+          ns <- map @{Compose} (\(rc, wb, n) => (rc, wb, piInfo.val, n)) $ pibindListName fname indents
           commitSymbol fname "}"
           commitSymbol fname "->"
           more <- go
@@ -1667,7 +1684,7 @@ implDecl fname indents
                          iname  <- optional $ decoratedSymbol fname "["
                                            *> decorate fname Function name
                                            <* decoratedSymbol fname "]"
-                         impls  <- implBinds fname indents
+                         impls  <- implBinds fname indents (isJust iname)
                          cons   <- constraints fname indents
                          n      <- decorate fname Typ name
                          params <- many (continue indents *> simpleExpr fname indents)
@@ -1685,7 +1702,7 @@ fieldDecl fname indents
       = do doc <- optDocumentation fname
            decoratedSymbol fname "{"
            commit
-           impl <- option Implicit (autoImplicitField <|> defImplicitField)
+           impl <- option Implicit (autoImplicitField fname indents <|> defImplicitField fname indents)
            fs <- fieldBody doc impl
            decoratedSymbol fname "}"
            atEnd indents
@@ -1695,16 +1712,6 @@ fieldDecl fname indents
            atEnd indents
            pure fs
   where
-    autoImplicitField : Rule (PiInfo t)
-    autoImplicitField = AutoImplicit <$ decoratedKeyword fname "auto"
-
-    defImplicitField : Rule (PiInfo PTerm)
-    defImplicitField = do
-      decoratedKeyword fname "default"
-      commit
-      t <- simpleExpr fname indents
-      pure (DefImplicit t)
-
     fieldBody : String -> PiInfo PTerm -> Rule (List PField)
     fieldBody doc p = do
       b <- bounds (do

src/Idris/Syntax.idr

@@ -447,7 +447,7 @@ mutual
                     PDecl' nm
        PImplementation : FC ->
                          Visibility -> List PFnOpt -> Pass ->
-                         (implicits : List (FC, RigCount, Name, PTerm' nm)) ->
+                         (implicits : List (FC, RigCount, Name, PiInfo (PTerm' nm), PTerm' nm)) ->
                          (constraints : List (Maybe Name, PTerm' nm)) ->
                          Name ->
                          (params : List (PTerm' nm)) ->

src/Idris/Syntax/Traversals.idr

@@ -327,11 +327,11 @@ mapPTermM f = goPTerm where
       (::) . (\ c => (a, b, c)) <$> goPTerm t
                                 <*> go3TupledPTerms ts
 
-    goImplicits : List (x, y, z, PTerm' nm) ->
-                      Core (List (x, y, z, PTerm' nm))
+    goImplicits : List (x, y, z, PiInfo (PTerm' nm), PTerm' nm) ->
+                      Core (List (x, y, z, PiInfo (PTerm' nm), PTerm' nm))
     goImplicits [] = pure []
-    goImplicits ((a, b, c, t) :: ts) =
-      ((::) . (a,b,c,)) <$> goPTerm t
+    goImplicits ((a, b, c, p, t) :: ts) =
+      ((::) . (a,b,c,)) <$> ((,) <$> goPiInfo p <*> goPTerm t)
                         <*> goImplicits ts
 
     go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) ->
@@ -576,9 +576,9 @@ mapPTerm f = goPTerm where
     go3TupledPTerms [] = []
     go3TupledPTerms ((a, b, t) :: ts) = (a, b, goPTerm t) :: go3TupledPTerms ts
 
-    goImplicits : List (x, y, z, PTerm' nm) -> List (x, y, z, PTerm' nm)
+    goImplicits : List (x, y, z, PiInfo (PTerm' nm), PTerm' nm) -> List (x, y, z, PiInfo (PTerm' nm), PTerm' nm)
     goImplicits [] = []
-    goImplicits ((a, b, c, t) :: ts) = (a,b,c, goPTerm t) :: goImplicits ts
+    goImplicits ((a, b, c, p, t) :: ts) = (a,b,c, goPiInfo p, goPTerm t) :: goImplicits ts
 
     go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) ->
                       List (x, y, PiInfo (PTerm' nm), PTerm' nm)

tests/idris2/interface/interface030/DefaultImplicitsInImpls.idr

@@ -0,0 +1,20 @@
+module DefaultImplicitsInImpls
+
+import Data.Vect
+
+%default total
+
+[TunableImpl] {default False fancy : Bool} -> Show Nat where
+  show x = if fancy then "!!! hohoho !!!" else "no fancy"
+
+X0 : String
+X0 = show @{TunableImpl} 5
+
+x0Corr : X0 === "no fancy"
+x0Corr = Refl
+
+X1 : String
+X1 = show @{TunableImpl {fancy=True}} 5
+
+x1Corr : X1 === "!!! hohoho !!!"
+x1Corr = Refl

tests/idris2/interface/interface030/expected

@@ -0,0 +1 @@
+1/1: Building DefaultImplicitsInImpls (DefaultImplicitsInImpls.idr)

tests/idris2/interface/interface030/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check DefaultImplicitsInImpls.idr