Fix parameter records (#3468)

* fix error location for errors in projection functions

* eta-expand both sides of the projection clauses

* testbuild

* Fixes to tests, virtualize FCs

* fix unelab issue

* update deriving tests

* remove TelNames

---------

Co-authored-by: Steve Dunham <[email protected]>

src/Core/Options/Log.idr

@@ -86,6 +86,8 @@ knownTopics = [
     ("declare.record.parameters", Just "Showing the implicitlty bound parameters"),
     ("declare.record.projection", Nothing),
     ("declare.record.projection.prefix", Nothing),
+    ("declare.record.projection.claim", Just "Showing the clause of an elaborated projection function"),
+    ("declare.record.projection.clause", Just "Showing the clause of an elaborated projection function"),
     ("declare.type", Nothing),
     ("desugar.idiom", Nothing),
     ("desugar.failing", Just "Log result of desugaring a `failing' block"),

src/Core/TT/Term.idr

@@ -556,3 +556,10 @@ covering
       showApp f args = "(" ++ assert_total (show f) ++ " " ++
                         assert_total (showSep " " (map show args))
                      ++ ")"
+
+||| Obtain the telescope of names and their types
+export
+collectPiNames : Term vars -> List (Bool, Name)
+collectPiNames (Bind _ nm (Pi _ _ Explicit ty) scope) = (False, nm) :: collectPiNames scope
+collectPiNames (Bind _ nm (Pi _ _ _ ty) scope) = (True, nm) :: (collectPiNames scope)
+collectPiNames _ = []

src/TTImp/ProcessRecord.idr

@@ -154,7 +154,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
                | Nothing => throw (InternalError "Missing data type \{show tn}, despite having just declared it!")
              log "declare.record" 20 "Obtained type: \{show ty}"
              (_ ** (tyenv, ty)) <- dropLeadingPis vars ty []
-             ty <- unelabNest !nestDrop tyenv ty
+             ty <- unelabNest (NoSugar True) !nestDrop tyenv ty
              log "declare.record.parameters" 30 "Unelaborated type: \{show ty}"
              params <- getParameters [<] ty
              addMissingNames ([<] <>< map fst params0) params []
@@ -259,7 +259,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
                    rfNameNS <- inCurrentNS (UN $ Field fldNameStr)
                    unNameNS <- inCurrentNS (UN $ Basic fldNameStr)
 
-                   ty <- unelabNest !nestDrop tyenv ty_chk
+                   ty <- unelabNest (NoSugar True) !nestDrop tyenv ty_chk
                    let ty' = substNames vars upds $ map rawName ty
                    log "declare.record.field" 5 $ "Field type: " ++ show ty'
                    let rname = MN "rec" 0
@@ -269,12 +269,12 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
                                  (map fst params ++ map fname fields ++ vars) $
                                       mkTy (paramTelescope params) $
                                       IPi bfc top Explicit (Just rname) (recTy tn params) ty'
-
+                   let fc' = virtualiseFC fc
                    let mkProjClaim = \ nm =>
-                          let ty = MkImpTy EmptyFC (NoFC nm) projTy
+                          let ty = MkImpTy fc' (MkFCVal fc' nm) projTy
                           in IClaim (MkFCVal bfc (MkIClaimData rig isVis [Inline] ty))
 
-                   log "declare.record.projection" 5 $
+                   log "declare.record.projection.claim" 5 $
                       "Projection " ++ show rfNameNS ++ " : " ++ show projTy
                    processDecl [] nest env (mkProjClaim rfNameNS)
 
@@ -283,16 +283,30 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
                           = apply (IVar bfc con)
                                     (replicate done (Implicit bfc True) ++
                                        (if imp == Explicit
-                                           then [IBindVar EmptyFC fldNameStr]
+                                           then [IBindVar fc' fldNameStr]
                                            else []) ++
                                     (replicate (countExp sc) (Implicit bfc True)))
                    let lhs = IApp bfc (IVar bfc rfNameNS)
                                 (if imp == Explicit
                                     then lhs_exp
                                     else INamedApp bfc lhs_exp (UN $ Basic fldNameStr)
                                              (IBindVar bfc fldNameStr))
-                   let rhs = IVar EmptyFC (UN $ Basic fldNameStr)
-                   log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs
+                   let rhs = IVar fc' (UN $ Basic fldNameStr)
+
+                   -- EtaExpand implicits on both sides:
+                   -- First, obtain all the implicit names in the prefix of
+                   let piNames = collectPiNames ty_chk
+
+                   let namesToRawImp : List (Bool, Name) -> (fn : RawImp) -> RawImp
+                       namesToRawImp ((True,  nm@(UN{})) :: xs) fn = namesToRawImp xs (INamedApp fc fn nm (IVar fc' nm))
+                       namesToRawImp _ fn = fn
+
+                   -- Then apply names for each argument to the lhs
+                   let lhs = namesToRawImp piNames lhs
+                   -- Do the same for the rhs
+                   let rhs = namesToRawImp piNames rhs
+
+                   log "declare.record.projection.clause" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs
                    processDecl [] nest env
                        (IDef bfc rfNameNS [PatClause bfc lhs rhs])
 

src/TTImp/Unelab.idr

@@ -30,6 +30,7 @@ used idx (TDelay _ _ _ tm) = used idx tm
 used idx (TForce _ _ tm) = used idx tm
 used idx _ = False
 
+public export
 data UnelabMode
      = Full
      | NoSugar Bool -- uniqify names
@@ -397,10 +398,11 @@ unelabNoPatvars env tm
 export
 unelabNest : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
+             UnelabMode ->
              List (Name, Nat) ->
              Env Term vars ->
              Term vars -> Core IRawImp
-unelabNest nest env (Meta fc n i args)
+unelabNest mode nest env (Meta fc n i args)
     = do let mkn = nameRoot n ++ showScope args
          pure (IHole fc mkn)
   where
@@ -415,13 +417,13 @@ unelabNest nest env (Meta fc n i args)
     showScope : List (Term vars) -> String
     showScope ts = " " ++ showNScope (mapMaybe toName ts)
 
-unelabNest nest env tm
-    = do tm' <- unelabTy Full nest env tm
+unelabNest mode nest env tm
+    = do tm' <- unelabTy mode nest env tm
          pure $ fst tm'
 
 export
 unelab : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          Env Term vars ->
          Term vars -> Core IRawImp
-unelab = unelabNest []
+unelab = unelabNest Full []

tests/base/deriving_foldable/expected

@@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
   foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
   foldMapIVect f (MkIVect x2) = foldMap f x2
 LOG derive.foldable.clauses:1: 
-  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5707} = eq} a -> b
+  foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5699} = eq} a -> b
   foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
 LOG derive.foldable.clauses:1: 
   foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b

tests/base/deriving_functor/expected

@@ -21,7 +21,7 @@ LOG derive.functor.clauses:1:
 LOG derive.functor.clauses:1: 
   mapBigTree : {0 a, b : Type} -> (a -> b) -> BigTree a -> BigTree b
   mapBigTree f (End x1) = End (f x1)
-  mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4047} => mapBigTree f (x3 {arg:4047}))
+  mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4042} => mapBigTree f (x3 {arg:4042}))
   mapBigTree f (Rose x1) = Rose (map (assert_total (mapBigTree f)) x1)
 LOG derive.functor.clauses:1: 
   mapMatrix : {0 m, n : _} -> {0 a, b : Type} -> (a -> b) -> Matrix m n a -> Matrix m n b
@@ -59,7 +59,7 @@ LOG derive.functor.clauses:1:
 LOG derive.functor.clauses:1: 
   mapFree : {0 f : _} -> {0 a, b : Type} -> (a -> b) -> Free f a -> Free f b
   mapFree f (Pure x2) = Pure (f x2)
-  mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5076} => mapFree f (x4 {arg:5076}))
+  mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5071} => mapFree f (x4 {arg:5071}))
 LOG derive.functor.assumption:10: I am assuming that the parameter m is a Functor
 LOG derive.functor.clauses:1: 
   mapMaybeT : {0 m : _} -> Functor m => {0 a, b : Type} -> (a -> b) -> MaybeT m a -> MaybeT m b
@@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
   mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
   mapIVect f (MkIVect x2) = MkIVect (map f x2)
 LOG derive.functor.clauses:1: 
-  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5692} = eq} a -> EqMap key {{conArg:5692} = eq} b
+  mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5684} = eq} a -> EqMap key {{conArg:5684} = eq} b
   mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
 LOG derive.functor.clauses:1: 
   mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
-  mapCont f (MkCont x2) = MkCont (\ {arg:6048} => x2 (\ {arg:6050} => {arg:6048} (f {arg:6050})))
+  mapCont f (MkCont x2) = MkCont (\ {arg:6040} => x2 (\ {arg:6042} => {arg:6040} (f {arg:6042})))
 LOG derive.functor.clauses:1: 
   mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
-  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6140} => \ {arg:6147} => x3 {arg:6140} (\ {arg:6149} => {arg:6147} (f {arg:6149})))
+  mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6132} => \ {arg:6139} => x3 {arg:6132} (\ {arg:6141} => {arg:6139} (f {arg:6141})))
 LOG derive.functor.clauses:1: 
   mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
-  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6254} => x3 (mapFst (\ t => \ {arg:6256} => t (f {arg:6256})) {arg:6254}))
+  mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6246} => x3 (mapFst (\ t => \ {arg:6248} => t (f {arg:6248})) {arg:6246}))
 LOG derive.functor.clauses:1: 
   mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
-  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6378} => x3 (Delay (mapFst (\ t => \ {arg:6381} => t (Delay (f {arg:6381}))) {arg:6378})))
+  mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6370} => x3 (Delay (mapFst (\ t => \ {arg:6373} => t (Delay (f {arg:6373}))) {arg:6370})))
 LOG derive.functor.clauses:1: 
   mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
   mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)

tests/base/deriving_show/expected

@@ -81,7 +81,7 @@ LOG derive.show.clauses:1:
 LOG derive.show.assumption:10: I am assuming that the parameter key can be shown
 LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
 LOG derive.show.clauses:1: 
-  showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5125} = eq} val -> String
+  showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5120} = eq} val -> String
   showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
 LOG derive.show.clauses:1: 
   showPrecX : Prec -> X -> String

tests/base/deriving_traversable/expected

@@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
   traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
   traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
 LOG derive.traversable.clauses:1: 
-  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13937} = eq} a -> f (EqMap key {{conArg:13937} = eq} b)
+  traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13929} = eq} a -> f (EqMap key {{conArg:13929} = eq} b)
   traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
 LOG derive.traversable.clauses:1: 
   traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)

tests/idris2/basic/basic044/expected

@@ -117,33 +117,33 @@ Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3:
 $resolved6
 $resolved7
-Target type : ?Vec.{a:4574}_[]
+Target type : ?Vec.{a:4569}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
 (($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
 (($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
 (($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
-Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
+Target type : (Vec.Vec ?Vec.{a:4569}_[] ?Vec.{n:4568}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5:
 (($resolved3 (fromInteger 0)) Nil)
 (($resolved4 (fromInteger 0)) Nil)
 (($resolved5 (fromInteger 0)) Nil)
-Target type : ?Vec.{a:4577}_[]
+Target type : ?Vec.{a:4572}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
   ($resolved1 0)
   ($resolved2 0)
-With default. Target type : ?Vec.{a:4579}_[]
+With default. Target type : ?Vec.{a:4574}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
 $resolved6
 $resolved7
-Target type : (Vec.Vec ?Vec.{a:4579}_[] ?Vec.{n:4578}_[])
+Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
   ($resolved1 0)
   ($resolved2 0)
-With default. Target type : ?Vec.{a:4578}_[]
+With default. Target type : ?Vec.{a:4573}_[]
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
 $resolved6
 $resolved7
-Target type : (Vec.Vec ?Vec.{a:4577}_[] ?Vec.{n:4576}_[])
+Target type : (Vec.Vec ?Vec.{a:4572}_[] ?Vec.{n:4571}_[])
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5:
 (($resolved4 (fromInteger 0)) Nil)
 Target type : (Prelude.Basics.List Prelude.Types.Nat)

tests/idris2/data/record019/expected

@@ -1,9 +1,9 @@
 1/1: Building BindParams (BindParams.idr)
-LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just a) %type (%pi RigW Explicit Nothing (Prelude.List a) (%pi RigW Explicit Nothing Prelude.Nat %type)))
+LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just a) %type (%pi RigW Explicit (Just xs) (Prelude.Basics.List a) (%pi RigW Explicit (Just n) Prelude.Types.Nat %type)))
 LOG declare.record.parameters:50: Decided to bind the following extra parameters:
   {0 a : %type}
 
-LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just n) Prelude.Nat (%pi Rig0 Implicit (Just a) %type (%pi Rig0 Implicit (Just xs) ((Main.Vect a) n) (%pi Rig0 Implicit (Just ys) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.(===) [a = ((Main.Vect a) n)]) xs) ys) (%pi RigW Explicit (Just zs) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.(===) [a = ((Main.Vect a) n)]) zs) xs) %type)))))))
+LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just n) Prelude.Types.Nat (%pi Rig0 Implicit (Just a) %type (%pi Rig0 Implicit (Just xs) ((Main.Vect a) n) (%pi Rig0 Implicit (Just ys) ((Main.Vect a) n) (%pi RigW Explicit (Just eq) (((Builtin.(===) [a = ((Main.Vect a) n)]) xs) ys) (%pi RigW Explicit (Just zs) ((Main.Vect a) n) (%pi RigW Explicit (Just eq2) (((Builtin.(===) [a = ((Main.Vect a) n)]) zs) xs) %type)))))))
 LOG declare.record.parameters:50: Decided to bind the following extra parameters:
   {0 n : Prelude.Types.Nat}
   {0 a : %type}
@@ -14,4 +14,4 @@ LOG declare.record.parameters:60: We elaborated Main.EtaProof in a non-empty loc
   Dropped: [b, a]
   Remaining type: (p : (Main.Product a[1] b[0])) -> Type
 
-LOG declare.record.parameters:30: Unelaborated type: (%pi RigW Explicit Nothing Main.Product %type)
+LOG declare.record.parameters:30: Unelaborated type: (%pi RigW Explicit (Just p) Main.Product %type)

tests/idris2/data/record021/RecordParam.idr

@@ -0,0 +1,4 @@
+record Ok (ty : Type) where
+  f : (x : ty) -> Type
+record Fail (ty : Type) where
+  f : {x : ty} -> Type

tests/idris2/data/record021/expected

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

tests/idris2/data/record021/run

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

tests/idris2/error/error018/expected

@@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7
 
 1/1: Building Issue1031-4 (Issue1031-4.idr)
 Error: While processing left hand side of nice. Unsolved holes:
-Main.{dotTm:820} introduced at: 
+Main.{dotTm:815} introduced at: 
 Issue1031-4:4:6--4:10
  1 | %default total
  2 |