Merge pull request #379 from edwinb/interface-type

Record implicit parameters of interfaces

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 34
+ttcVersion = 35
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Idris/Elab/Implementation.idr

@@ -182,7 +182,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
 
                -- 2. Elaborate top level function types for this interface
                defs <- get Ctxt
-               fns <- topMethTypes [] impName methImps impsp (params cdata)
+               fns <- topMethTypes [] impName methImps impsp
+                                      (implParams cdata) (params cdata)
                                       (map fst (methods cdata))
                                       (methods cdata)
                traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
@@ -316,11 +317,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     -- in later method types (specifically, putting implicits in)
     topMethType : List (Name, RawImp) ->
                   Name -> List (Name, RigCount, RawImp) ->
-                  List String -> List Name -> List Name ->
+                  List String -> List Name -> List Name -> List Name ->
                   (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
                   Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
                            List (Name, RawImp))
-    topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
+    topMethType methupds impName methImps impsp imppnames pnames allmeths (mn, c, treq, (d, mty_in))
         = do -- Get the specialised type by applying the method to the
              -- parameters
              n <- inCurrentNS (methName mn)
@@ -335,9 +336,23 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
              -- parameters are passed through to any earlier methods which
              -- appear in the type
              let mty_in = substNames vars methupds mty_in
+
+             -- Substitute _ in for the implicit parameters, then
+             -- substitute in the explicit parameters.
+             let mty_iparams
+                   = substBindVars vars
+                                (map (\n => (n, Implicit fc False)) imppnames)
+                                mty_in
+             let mty_params
+                   = substNames vars (zip pnames ps) mty_iparams
+             log 5 $ "Substitute implicits " ++ show imppnames ++
+                     " parameters " ++ show (zip pnames ps) ++
+                     " "  ++ show mty_in ++ " is " ++
+                     show mty_params
+
              let mbase = bindImps methImps $
                          bindConstraints fc AutoImplicit cons $
-                         substNames vars (zip pnames ps) mty_in
+                         mty_params
              let ibound = findImplicits mbase
 
              mty <- bindTypeNamesUsed ibound vars mbase
@@ -358,13 +373,14 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
 
     topMethTypes : List (Name, RawImp) ->
                    Name -> List (Name, RigCount, RawImp) ->
-                   List String -> List Name -> List Name ->
+                   List String ->
+                   List Name -> List Name -> List Name ->
                    List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
                    Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
-    topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
+    topMethTypes upds impName methImps impsp imppnames pnames allmeths [] = pure []
-    topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
+    topMethTypes upds impName methImps impsp imppnames pnames allmeths (m :: ms)
-        = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
+        = do (m', newupds) <- topMethType upds impName methImps impsp imppnames pnames allmeths m
-             ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
+             ms' <- topMethTypes (newupds ++ upds) impName methImps impsp imppnames pnames allmeths ms
              pure (m' :: ms')
 
     mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl

src/Idris/Elab/Interface.idr

@@ -7,6 +7,7 @@ import Core.Env
 import Core.Metadata
 import Core.TT
 import Core.Unify
+import Core.Value
 
 import Idris.Resugar
 import Idris.Syntax
@@ -230,13 +231,13 @@ mkCon loc n
 
 updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
-                 Name -> Name -> List Name -> List RawImp ->
+                 Name -> Name -> List Name -> List Name -> List RawImp ->
                  List (Name, RigCount, List FnOpt, (Bool, RawImp)) -> List (Name, List ImpClause) ->
                  Core ()
-updateIfaceSyn iname cn ps cs ms ds
+updateIfaceSyn iname cn impps ps cs ms ds
     = do syn <- get Syn
          ms' <- traverse totMeth ms
-         let info = MkIFaceInfo cn ps cs ms' ds
+         let info = MkIFaceInfo cn impps ps cs ms' ds
          put Syn (record { ifaces $= addName iname info } syn)
  where
     findSetTotal : List FnOpt -> Maybe TotalReq
@@ -250,6 +251,13 @@ updateIfaceSyn iname cn ps cs ms ds
         = do let treq = findSetTotal opts
              pure (n, c, treq, t)
 
+-- Read the implicitly added parameters from an interface type, so that we
+-- know to substitute an implicit in when defining the implementation
+getImplParams : Term vars -> List Name
+getImplParams (Bind _ n (Pi _ Implicit _) sc)
+    = n :: getImplParams sc
+getImplParams _ = []
+
 export
 elabInterface : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
@@ -267,6 +275,7 @@ elabInterface : {vars : _} ->
                 Core ()
 elabInterface {vars} fc vis env nest constraints iname params dets mcon body
     = do fullIName <- getFullName iname
+         ns_iname <- inCurrentNS fullIName
          let conName_in = maybe (mkCon fc fullIName) id mcon
          -- Machine generated names need to be qualified when looking them up
          conName <- inCurrentNS conName_in
@@ -282,9 +291,13 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
 
          ns_meths <- traverse (\mt => do n <- inCurrentNS (fst mt)
                                          pure (n, snd mt)) meth_decls
-         ns_iname <- inCurrentNS fullIName
+         defs <- get Ctxt
+         Just ty <- lookupTyExact ns_iname (gamma defs)
+              | Nothing => throw (UndefinedName fc iname)
+         let implParams = getImplParams ty
+
          updateIfaceSyn ns_iname conName
-                        (map fst params) (map snd constraints)
+                        implParams (map fst params) (map snd constraints)
                         ns_meths ds
   where
     nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)

src/Idris/Syntax.idr

@@ -593,6 +593,7 @@ public export
 record IFaceInfo where
   constructor MkIFaceInfo
   iconstructor : Name
+  implParams : List Name
   params : List Name
   parents : List RawImp
   methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp)
@@ -601,8 +602,9 @@ record IFaceInfo where
 
 export
 TTC IFaceInfo where
-  toBuf b (MkIFaceInfo ic ps cs ms ds)
+  toBuf b (MkIFaceInfo ic impps ps cs ms ds)
       = do toBuf b ic
+           toBuf b impps
            toBuf b ps
            toBuf b cs
            toBuf b ms
@@ -610,11 +612,12 @@ TTC IFaceInfo where
 
   fromBuf b
       = do ic <- fromBuf b
+           impps <- fromBuf b
            ps <- fromBuf b
            cs <- fromBuf b
            ms <- fromBuf b
            ds <- fromBuf b
-           pure (MkIFaceInfo ic ps cs ms ds)
+           pure (MkIFaceInfo ic impps ps cs ms ds)
 
 -- If you update this, update 'extendAs' in Desugar to keep it up to date
 -- when reading imports

src/TTImp/Utils.idr

@@ -88,8 +88,6 @@ findAllNames env (IWithApp fc fn av)
     = findAllNames env fn ++ findAllNames env av
 findAllNames env (IAs fc _ n pat)
     = n :: findAllNames env pat
-findAllNames env (IAs fc _ n pat)
-    = findAllNames env pat
 findAllNames env (IMustUnify fc r pat)
     = findAllNames env pat
 findAllNames env (IDelayed fc r t)
@@ -137,97 +135,117 @@ findIBindVars (IAlternative fc u alts)
 findIBindVars tm = []
 
 mutual
-  export
+  -- Substitute for either an explicit variable name, or a bound variable name
-  substNames : List Name -> List (Name, RawImp) ->
+  substNames' : Bool -> List Name -> List (Name, RawImp) ->
-               RawImp -> RawImp
+                RawImp -> RawImp
-  substNames bound ps (IVar fc n)
+  substNames' False bound ps (IVar fc n)
       = if not (n `elem` bound)
            then case lookup n ps of
                      Just t => t
                      _ => IVar fc n
            else IVar fc n
-  substNames bound ps (IPi fc r p mn argTy retTy)
+  substNames' True bound ps (IBindVar fc n)
+      = if not (UN n `elem` bound)
+           then case lookup (UN n) ps of
+                     Just t => t
+                     _ => IBindVar fc n
+           else IBindVar fc n
+  substNames' bvar bound ps (IPi fc r p mn argTy retTy)
       = let bound' = maybe bound (\n => n :: bound) mn in
-            IPi fc r p mn (substNames bound ps argTy)
+            IPi fc r p mn (substNames' bvar bound ps argTy)
-                          (substNames bound' ps retTy)
+                          (substNames' bvar bound' ps retTy)
-  substNames bound ps (ILam fc r p mn argTy scope)
+  substNames' bvar bound ps (ILam fc r p mn argTy scope)
       = let bound' = maybe bound (\n => n :: bound) mn in
-            ILam fc r p mn (substNames bound ps argTy)
+            ILam fc r p mn (substNames' bvar bound ps argTy)
-                           (substNames bound' ps scope)
+                           (substNames' bvar bound' ps scope)
-  substNames bound ps (ILet fc r n nTy nVal scope)
+  substNames' bvar bound ps (ILet fc r n nTy nVal scope)
       = let bound' = n :: bound in
-            ILet fc r n (substNames bound ps nTy)
+            ILet fc r n (substNames' bvar bound ps nTy)
-                        (substNames bound ps nVal)
+                        (substNames' bvar bound ps nVal)
-                        (substNames bound' ps scope)
+                        (substNames' bvar bound' ps scope)
-  substNames bound ps (ICase fc y ty xs)
+  substNames' bvar bound ps (ICase fc y ty xs)
-      = ICase fc (substNames bound ps y) (substNames bound ps ty)
+      = ICase fc (substNames' bvar bound ps y) (substNames' bvar bound ps ty)
-                 (map (substNamesClause bound ps) xs)
+                 (map (substNamesClause' bvar bound ps) xs)
-  substNames bound ps (ILocal fc xs y)
+  substNames' bvar bound ps (ILocal fc xs y)
       = let bound' = definedInBlock [] xs ++ bound in
-            ILocal fc (map (substNamesDecl bound ps) xs)
+            ILocal fc (map (substNamesDecl' bvar bound ps) xs)
-                      (substNames bound' ps y)
+                      (substNames' bvar bound' ps y)
-  substNames bound ps (IApp fc fn arg)
+  substNames' bvar bound ps (IApp fc fn arg)
-      = IApp fc (substNames bound ps fn) (substNames bound ps arg)
+      = IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
-  substNames bound ps (IImplicitApp fc fn y arg)
+  substNames' bvar bound ps (IImplicitApp fc fn y arg)
-      = IImplicitApp fc (substNames bound ps fn) y (substNames bound ps arg)
+      = IImplicitApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
-  substNames bound ps (IWithApp fc fn arg)
+  substNames' bvar bound ps (IWithApp fc fn arg)
-      = IWithApp fc (substNames bound ps fn) (substNames bound ps arg)
+      = IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
-  substNames bound ps (IAlternative fc y xs)
+  substNames' bvar bound ps (IAlternative fc y xs)
-      = IAlternative fc y (map (substNames bound ps) xs)
+      = IAlternative fc y (map (substNames' bvar bound ps) xs)
-  substNames bound ps (ICoerced fc y)
+  substNames' bvar bound ps (ICoerced fc y)
-      = ICoerced fc (substNames bound ps y)
+      = ICoerced fc (substNames' bvar bound ps y)
-  substNames bound ps (IAs fc s y pattern)
+  substNames' bvar bound ps (IAs fc s y pattern)
-      = IAs fc s y (substNames bound ps pattern)
+      = IAs fc s y (substNames' bvar bound ps pattern)
-  substNames bound ps (IMustUnify fc r pattern)
+  substNames' bvar bound ps (IMustUnify fc r pattern)
-      = IMustUnify fc r (substNames bound ps pattern)
+      = IMustUnify fc r (substNames' bvar bound ps pattern)
-  substNames bound ps (IDelayed fc r t)
+  substNames' bvar bound ps (IDelayed fc r t)
-      = IDelayed fc r (substNames bound ps t)
+      = IDelayed fc r (substNames' bvar bound ps t)
-  substNames bound ps (IDelay fc t)
+  substNames' bvar bound ps (IDelay fc t)
-      = IDelay fc (substNames bound ps t)
+      = IDelay fc (substNames' bvar bound ps t)
-  substNames bound ps (IForce fc t)
+  substNames' bvar bound ps (IForce fc t)
-      = IForce fc (substNames bound ps t)
+      = IForce fc (substNames' bvar bound ps t)
-  substNames bound ps tm = tm
+  substNames' bvar bound ps tm = tm
 
-  export
+  substNamesClause' : Bool -> List Name -> List (Name, RawImp) ->
-  substNamesClause : List Name -> List (Name, RawImp) ->
+                      ImpClause -> ImpClause
-                     ImpClause -> ImpClause
+  substNamesClause' bvar bound ps (PatClause fc lhs rhs)
-  substNamesClause bound ps (PatClause fc lhs rhs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
                         ++ bound in
-            PatClause fc (substNames [] [] lhs)
+            PatClause fc (substNames' bvar [] [] lhs)
-                         (substNames bound' ps rhs)
+                         (substNames' bvar bound' ps rhs)
-  substNamesClause bound ps (WithClause fc lhs wval flags cs)
+  substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
                         ++ bound in
-            WithClause fc (substNames [] [] lhs)
+            WithClause fc (substNames' bvar [] [] lhs)
-                          (substNames bound' ps wval) flags cs
+                          (substNames' bvar bound' ps wval) flags cs
-  substNamesClause bound ps (ImpossibleClause fc lhs)
+  substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
-      = ImpossibleClause fc (substNames bound [] lhs)
+      = ImpossibleClause fc (substNames' bvar bound [] lhs)
 
-  substNamesTy : List Name -> List (Name, RawImp) ->
+  substNamesTy' : Bool -> List Name -> List (Name, RawImp) ->
                   ImpTy -> ImpTy
-  substNamesTy bound ps (MkImpTy fc n ty)
+  substNamesTy' bvar bound ps (MkImpTy fc n ty)
-      = MkImpTy fc n (substNames bound ps ty)
+      = MkImpTy fc n (substNames' bvar bound ps ty)
 
-  substNamesData : List Name -> List (Name, RawImp) ->
+  substNamesData' : Bool -> List Name -> List (Name, RawImp) ->
-                   ImpData -> ImpData
+                    ImpData -> ImpData
-  substNamesData bound ps (MkImpData fc n con opts dcons)
+  substNamesData' bvar bound ps (MkImpData fc n con opts dcons)
-      = MkImpData fc n (substNames bound ps con) opts
+      = MkImpData fc n (substNames' bvar bound ps con) opts
-                  (map (substNamesTy bound ps) dcons)
+                  (map (substNamesTy' bvar bound ps) dcons)
-  substNamesData bound ps (MkImpLater fc n con)
+  substNamesData' bvar bound ps (MkImpLater fc n con)
-      = MkImpLater fc n (substNames bound ps con)
+      = MkImpLater fc n (substNames' bvar bound ps con)
 
-  substNamesDecl : List Name -> List (Name, RawImp ) ->
+  substNamesDecl' : Bool -> List Name -> List (Name, RawImp ) ->
                    ImpDecl -> ImpDecl
-  substNamesDecl bound ps (IClaim fc r vis opts td)
+  substNamesDecl' bvar bound ps (IClaim fc r vis opts td)
-      = IClaim fc r vis opts (substNamesTy bound ps td)
+      = IClaim fc r vis opts (substNamesTy' bvar bound ps td)
-  substNamesDecl bound ps (IDef fc n cs)
+  substNamesDecl' bvar bound ps (IDef fc n cs)
-      = IDef fc n (map (substNamesClause bound ps) cs)
+      = IDef fc n (map (substNamesClause' bvar bound ps) cs)
-  substNamesDecl bound ps (IData fc vis d)
+  substNamesDecl' bvar bound ps (IData fc vis d)
-      = IData fc vis (substNamesData bound ps d)
+      = IData fc vis (substNamesData' bvar bound ps d)
-  substNamesDecl bound ps (INamespace fc ns ds)
+  substNamesDecl' bvar bound ps (INamespace fc ns ds)
-      = INamespace fc ns (map (substNamesDecl bound ps) ds)
+      = INamespace fc ns (map (substNamesDecl' bvar bound ps) ds)
-  substNamesDecl bound ps d = d
+  substNamesDecl' bvar bound ps d = d
+
+export
+substNames : List Name -> List (Name, RawImp) ->
+             RawImp -> RawImp
+substNames = substNames' False
+
+export
+substBindVars : List Name -> List (Name, RawImp) ->
+                RawImp -> RawImp
+substBindVars = substNames' True
+
+export
+substNamesClause : List Name -> List (Name, RawImp) ->
+                   ImpClause -> ImpClause
+substNamesClause = substNamesClause' False
 
 mutual
   export

tests/Main.idr

@@ -97,7 +97,7 @@ idrisTests
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
-       "reg022", "reg023", "reg024", "reg025",
+       "reg022", "reg023", "reg024", "reg025", "reg026",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",

tests/idris2/reg026/Meh.idr

@@ -0,0 +1,12 @@
+module Meh
+
+import public Control.WellFounded
+
+public export
+interface Argh (rel : a -> a -> Type) where
+  argh : (x : a) -> Accessible rel x
+
+data Meh : Nat -> Nat -> Type where
+
+implementation Argh Meh where
+  argh x = ?foo

tests/idris2/reg026/expected

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

tests/idris2/reg026/run

@@ -0,0 +1,3 @@
+$1 --check Meh.idr
+
+rm -rf build