[ fix ] Fix interface elaboration when %unbound_implicits is off

CHANGELOG.md

@@ -101,6 +101,8 @@
 
 * Fixed a bug that caused `f` to sometimes be replaced by `fx` after matching `fx = f x`.
 
+* Fixed elaboration of interfaces when `%unbound_implicits` is turned off.
+
 ### Library changes
 
 #### Prelude

src/Idris/Elab/Interface.idr

@@ -248,17 +248,17 @@ getConstraintHint : {vars : _} ->
                     Name -> Name ->
                     (constraints : List Name) ->
                     (allmeths : List Name) ->
-                    (params : List Name) ->
+                    (params : List (Name, (RigCount, RawImp))) ->
                     (Name, RawImp) -> Core (Name, List ImpDecl)
 getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)
-    = do let ity = apply (IVar fc iname) (map (IVar fc) params)
+    = do let ity = apply (IVar fc iname) (map (IVar fc . fst) params)
          let fty = IPi fc top Explicit Nothing ity con
          ty_imp <- bindTypeNames fc [] (meths ++ vars) fty
          let hintname = DN ("Constraint " ++ show con)
                           (UN (Basic $ "__" ++ show iname ++ "_" ++ show con))
 
          let tydecl = IClaim fc top vis [Inline, Hint False]
-                          (MkImpTy EmptyFC EmptyFC hintname ty_imp)
+                          (MkImpTy EmptyFC EmptyFC hintname (bindPs params ty_imp))
 
          let conapp = apply (impsBind (IVar fc cname) (map bindName constraints))
                               (map (const (Implicit fc True)) meths)
@@ -281,6 +281,10 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
     impsBind fn (n :: ns)
         = impsBind (IAutoApp fc fn (IBindVar fc n)) ns
 
+    bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
+    bindPs [] ty = ty
+    bindPs ((n, (rig, pty)) :: ps) ty
+        = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
 
 getDefault : ImpDecl -> Maybe (FC, List FnOpt, Name, List ImpClause)
 getDefault (IDef fc n cs) = Just (fc, [], n, cs)
@@ -519,7 +523,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
              chints <- traverse (getConstraintHint vfc env vis iname conName
                                                  (map fst nconstraints)
                                                  meth_names
-                                                 paramNames) nconstraints
+                                                 params) nconstraints
              log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints
              traverse_ (processDecl [] nest env) (concatMap snd chints)
              traverse_ (\n => do mn <- inCurrentNS n

tests/Main.idr

@@ -125,7 +125,7 @@ idrisTestsInterface = MkTestPool "Interface" [] Nothing
        "interface017", "interface018", "interface019", "interface020",
        "interface021", "interface022", "interface023", "interface024",
        "interface025", "interface026", "interface027", "interface028",
-       "interface029"]
+       "interface029", "interface030" ]
 
 idrisTestsLinear : TestPool
 idrisTestsLinear = MkTestPool "Quantities" [] Nothing

tests/idris2/interface030/NoUnbound.idr

@@ -0,0 +1,3 @@
+%unbound_implicits off
+interface Foo a where
+interface Foo a => Bar (a : Type) where

tests/idris2/interface030/expected

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

tests/idris2/interface030/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 --check NoUnbound.idr

tests/idris2/spec001/expected

@@ -27,18 +27,18 @@ LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:2} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:2}[0]) t[2]))
 LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
 1/1: Building Desc2 (Desc2.idr)
-LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8747}[0]))), (3, Dynamic)
+LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8766} : a[0]) -> b[2]) => \({arg:8771} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8771}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
-(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
+(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8820} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
 LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e:
-((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) alg)) t))
-LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8747}[0]))), (3, Dynamic)
+((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8820} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8766}) a b) (%lam RigW Explicit (Just {arg:8771}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8771}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8766}) a b) (%lam RigW Explicit (Just {arg:8771}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8771}))))))]) alg)) t))
+LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8766} : a[0]) -> b[2]) => \({arg:8771} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8771}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
-(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
+(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8820} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
 LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761:
-((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) alg)) t))
+((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8820} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8766}) a b) (%lam RigW Explicit (Just {arg:8771}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8771}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8766}) a b) (%lam RigW Explicit (Just {arg:8771}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8771}))))))]) alg)) t))
 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761