[ fix ] holes in record types

idris2api.ipkg

@@ -257,6 +257,7 @@ modules =
     TTImp.Reflect,
     TTImp.TTImp,
     TTImp.TTImp.Functor,
+    TTImp.TTImp.Traversals,
     TTImp.TTImp.TTC,
     TTImp.Unelab,
     TTImp.Utils,

src/TTImp/ProcessRecord.idr

@@ -14,6 +14,7 @@ import TTImp.BindImplicits
 import TTImp.Elab.Check
 import TTImp.TTImp
 import TTImp.TTImp.Functor
+import TTImp.TTImp.Traversals
 import TTImp.Unelab
 import TTImp.Utils
 
@@ -21,10 +22,17 @@ import Data.List
 
 %default covering
 
+-- Used to remove the holes so that we don't end up with "hole is already defined"
+-- errors because they've been duplicarted when forming the various types of the
+-- record constructor, getters, etc.
+killHole : RawImp -> RawImp
+killHole (IHole fc str) = Implicit fc True
+killHole t = t
+
 mkDataTy : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
 mkDataTy fc [] = IType fc
 mkDataTy fc ((n, c, p, ty) :: ps)
-    = IPi fc c p (Just n) ty (mkDataTy fc ps)
+    = IPi fc c (mapPiInfo killHole p) (Just n) (mapTTImp killHole ty) (mkDataTy fc ps)
 
 -- Projections are only visible if the record is public export
 projVis : Visibility -> Visibility
@@ -72,6 +80,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel
                                     nestedNS := newns :: nns }
 
   where
+
     paramTelescope : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp)
     paramTelescope = map jname params
       where
@@ -81,6 +90,10 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel
         -- and projections
         jname (n, _, _, t) = (EmptyFC, Just n, erased, Implicit, t)
 
+    removeIHoles : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp) ->
+                   List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp)
+    removeIHoles = map (map $ map $ map $ bimap (mapPiInfo killHole) (mapTTImp killHole))
+
     fname : IField -> Name
     fname (MkIField fc c p n ty) = n
 
@@ -104,6 +117,9 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel
         apply f ((n, arg, Explicit) :: xs) = apply (IApp         (getFC f) f          arg) xs
         apply f ((n, arg, _       ) :: xs) = apply (INamedApp (getFC f) f n arg) xs
 
+    paramNames : List Name
+    paramNames = map fst params
+
     elabAsData : (tn : Name) -> -- fully qualified name of the record type
                  (conName : Name) -> -- fully qualified name of the record type constructor
                  Core ()
@@ -111,11 +127,10 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel
         = do let fc = virtualiseFC fc
              let conty = mkTy paramTelescope $
                          mkTy (map farg fields) (recTy tn)
-             let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] (map fst params ++
-                                           map fname fields ++ vars) conty)
-             let dt = MkImpData fc tn !(bindTypeNames fc [] (map fst params ++
-                                           map fname fields ++ vars)
-                                         (mkDataTy fc params)) [] [con]
+             let boundNames = paramNames ++ map fname fields ++ vars
+             let con = MkImpTy EmptyFC EmptyFC cname
+                       !(bindTypeNames fc [] boundNames conty)
+             let dt = MkImpData fc tn !(bindTypeNames fc [] boundNames (mkDataTy fc params)) [] [con]
              log "declare.record" 5 $ "Record data type " ++ show dt
              processDecl [] nest env (IData fc vis mbtot dt)
 
@@ -163,7 +178,9 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params conName_in fiel
                    -- Claim the projection type
                    projTy <- bindTypeNames fc []
                                  (map fst params ++ map fname fields ++ vars) $
-                                    mkTy paramTelescope $
+                                    -- Remove the holes here so that we don't end up with
+                                    -- "hole is already defined" errors
+                                      mkTy (removeIHoles paramTelescope) $
                                       IPi bfc top Explicit (Just rname) (recTy tn) ty'
 
                    let mkProjClaim = \ nm =>

src/TTImp/TTImp/Traversals.idr

@@ -0,0 +1,128 @@
+module TTImp.TTImp.Traversals
+
+import Core.TT
+import TTImp.TTImp
+
+%default total
+
+parameters (f : RawImp' nm -> RawImp' nm)
+
+  export
+  mapTTImp :RawImp' nm -> RawImp' nm
+
+  export
+  mapPiInfo : PiInfo (RawImp' nm) -> PiInfo (RawImp' nm)
+  mapPiInfo Implicit = Implicit
+  mapPiInfo Explicit = Explicit
+  mapPiInfo AutoImplicit = AutoImplicit
+  mapPiInfo (DefImplicit t) = DefImplicit (mapTTImp t)
+
+  export
+  mapImpClause : ImpClause' nm -> ImpClause' nm
+  mapImpClause (PatClause fc lhs rhs) = PatClause fc (mapTTImp lhs) (mapTTImp rhs)
+  mapImpClause (WithClause fc lhs rig wval prf flags cls)
+    = WithClause fc (mapTTImp lhs) rig (mapTTImp wval) prf flags (assert_total $ map mapImpClause cls)
+  mapImpClause (ImpossibleClause fc lhs) = ImpossibleClause fc (mapTTImp lhs)
+
+  export
+  mapImpTy : ImpTy' nm -> ImpTy' nm
+  mapImpTy (MkImpTy fc nameFC n ty) = MkImpTy fc nameFC n (mapTTImp ty)
+
+  export
+  mapFnOpt : FnOpt' nm -> FnOpt' nm
+  mapFnOpt Inline = Inline
+  mapFnOpt NoInline = NoInline
+  mapFnOpt Deprecate = Deprecate
+  mapFnOpt TCInline = TCInline
+  mapFnOpt (Hint b) = Hint b
+  mapFnOpt (GlobalHint b) = GlobalHint b
+  mapFnOpt ExternFn = ExternFn
+  mapFnOpt (ForeignFn ts) = ForeignFn (map mapTTImp ts)
+  mapFnOpt (ForeignExport ts) = ForeignExport (map mapTTImp ts)
+  mapFnOpt Invertible = Invertible
+  mapFnOpt (Totality treq) = Totality treq
+  mapFnOpt Macro = Macro
+  mapFnOpt (SpecArgs ns) = SpecArgs ns
+  mapFnOpt (NoMangle mdir) = NoMangle mdir
+
+  export
+  mapImpData : ImpData' nm -> ImpData' nm
+  mapImpData (MkImpData fc n tycon opts datacons)
+    = MkImpData fc n (mapTTImp tycon) opts (map mapImpTy datacons)
+  mapImpData (MkImpLater fc n tycon) = MkImpLater fc n (mapTTImp tycon)
+
+  export
+  mapIField : IField' nm -> IField' nm
+  mapIField (MkIField fc rig pinfo n t) = MkIField fc rig (mapPiInfo pinfo) n (mapTTImp t)
+
+  export
+  mapImpRecord : ImpRecord' nm -> ImpRecord' nm
+  mapImpRecord (MkImpRecord fc n params conName fields)
+    = MkImpRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) conName (map mapIField fields)
+
+  export
+  mapImpDecl : ImpDecl' nm -> ImpDecl' nm
+  mapImpDecl (IClaim fc rig vis opts ty)
+    = IClaim fc rig vis (map mapFnOpt opts) (mapImpTy ty)
+  mapImpDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapImpData dat)
+  mapImpDecl (IDef fc n cls) = IDef fc n (map mapImpClause cls)
+  mapImpDecl (IParameters fc params xs) = IParameters fc params (assert_total $ map mapImpDecl xs)
+  mapImpDecl (IRecord fc mstr x y rec) = IRecord fc mstr x y (mapImpRecord rec)
+  mapImpDecl (IFail fc mstr xs) = IFail fc mstr (assert_total $ map mapImpDecl xs)
+  mapImpDecl (INamespace fc mi xs) = INamespace fc mi (assert_total $ map mapImpDecl xs)
+  mapImpDecl (ITransform fc n t u) = ITransform fc n (mapTTImp t) (mapTTImp u)
+  mapImpDecl (IRunElabDecl fc t) = IRunElabDecl fc (mapTTImp t)
+  mapImpDecl (IPragma ns g) = IPragma ns g
+  mapImpDecl (ILog x) = ILog x
+  mapImpDecl (IBuiltin fc x n) = IBuiltin fc x n
+
+  export
+  mapIFieldUpdate : IFieldUpdate' nm -> IFieldUpdate' nm
+  mapIFieldUpdate (ISetField path t) = ISetField path (mapTTImp t)
+  mapIFieldUpdate (ISetFieldApp path t) = ISetFieldApp path (mapTTImp t)
+
+  export
+  mapAltType : AltType' nm -> AltType' nm
+  mapAltType FirstSuccess = FirstSuccess
+  mapAltType Unique = Unique
+  mapAltType (UniqueDefault t) = UniqueDefault (mapTTImp t)
+
+  mapTTImp t@(IVar _ _) = f t
+  mapTTImp (IPi fc rig pinfo x argTy retTy)
+    = f $ IPi fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp retTy)
+  mapTTImp (ILam fc rig pinfo x argTy lamTy)
+    = f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy)
+  mapTTImp (ILet fc lhsFC rig n nTy nVal scope)
+    = f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope)
+  mapTTImp (ICase fc t ty cls)
+    = f $ ICase fc (mapTTImp t) (mapTTImp ty) (assert_total $ map mapImpClause cls)
+  mapTTImp (ILocal fc xs t)
+    = f $ ILocal fc (assert_total $ map mapImpDecl xs) (mapTTImp t)
+  mapTTImp (ICaseLocal fc unm inm args t) = f $ ICaseLocal fc unm inm args (mapTTImp t)
+  mapTTImp (IUpdate fc upds t) = f $ IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t)
+  mapTTImp (IApp fc t u) = f $ IApp fc (mapTTImp t) (mapTTImp u)
+  mapTTImp (IAutoApp fc t u) = f $ IAutoApp fc (mapTTImp t) (mapTTImp u)
+  mapTTImp (INamedApp fc t n u) = f $ INamedApp fc (mapTTImp t) n (mapTTImp u)
+  mapTTImp (IWithApp fc t u) = f $ IWithApp fc (mapTTImp t) (mapTTImp u)
+  mapTTImp (ISearch fc depth) = f $ ISearch fc depth
+  mapTTImp (IAlternative fc alt ts) = f $ IAlternative fc (mapAltType alt) (assert_total map mapTTImp ts)
+  mapTTImp (IRewrite fc t u) = f $ IRewrite fc (mapTTImp t) (mapTTImp u)
+  mapTTImp (ICoerced fc t) = f $ ICoerced fc (mapTTImp t)
+  mapTTImp (IBindHere fc bm t) = f $ IBindHere fc bm (mapTTImp t)
+  mapTTImp (IBindVar fc str) = f $ IBindVar fc str
+  mapTTImp (IAs fc nameFC side n t) = f $ IAs fc nameFC side n (mapTTImp t)
+  mapTTImp (IMustUnify fc x t) = f $ IMustUnify fc x (mapTTImp t)
+  mapTTImp (IDelayed fc lz t) = f $ IDelayed fc lz (mapTTImp t)
+  mapTTImp (IDelay fc t) = f $ IDelay fc (mapTTImp t)
+  mapTTImp (IForce fc t) = f $ IForce fc (mapTTImp t)
+  mapTTImp (IQuote fc t) = f $ IQuote fc (mapTTImp t)
+  mapTTImp (IQuoteName fc n) = f $ IQuoteName fc n
+  mapTTImp (IQuoteDecl fc xs) = f $ IQuoteDecl fc (assert_total $ map mapImpDecl xs)
+  mapTTImp (IUnquote fc t) = f $ IUnquote fc (mapTTImp t)
+  mapTTImp (IRunElab fc t) = f $ IRunElab fc (mapTTImp t)
+  mapTTImp (IPrimVal fc c) = f $ IPrimVal fc c
+  mapTTImp (IType fc) = f $ IType fc
+  mapTTImp (IHole fc str) = f $ IHole fc str
+  mapTTImp (IUnifyLog fc x t) = f $ IUnifyLog fc x (mapTTImp t)
+  mapTTImp (Implicit fc bindIfUnsolved) = f $ Implicit fc bindIfUnsolved
+  mapTTImp (IWithUnambigNames fc xs t) = f $ IWithUnambigNames fc xs (mapTTImp t)

tests/Main.idr

@@ -157,7 +157,8 @@ idrisTestsData = MkTestPool "Data and record types" [] Nothing
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004", "record005",
        "record006", "record007", "record008", "record009", "record010",
-       "record011", "record012", "record013", "record014", "record015" ]
+       "record011", "record012", "record013", "record014", "record015",
+       "record016" ]
 
 idrisTestsBuiltin : TestPool
 idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing

tests/idris2/record016/HoleRecord.idr

@@ -0,0 +1,9 @@
+record Wrap (a : ?hole) where
+  constructor MkWrap
+  proj : a
+
+record Unit (a : ?hole2) where
+  constructor MkUnit
+
+record Tree (a : ?hole3) where
+  isThree : 3 === a

tests/idris2/record016/expected

@@ -0,0 +1,7 @@
+1/1: Building HoleRecord (HoleRecord.idr)
+Main> Main.hole : Type
+Main> Main.hole2 : Type
+Main> Main.hole3 : Type
+Main> 1 hole: Main.hole2 : Type
+Main> 
+Bye for now!

tests/idris2/record016/input

@@ -0,0 +1,4 @@
+:t hole
+:t hole2
+:t hole3
+:m

tests/idris2/record016/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner HoleRecord.idr < input