Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Investigate suspicious location tracking #3409

Open
andrevidela opened this issue Oct 30, 2024 · 1 comment
Open

Investigate suspicious location tracking #3409

andrevidela opened this issue Oct 30, 2024 · 1 comment

Comments

@andrevidela
Copy link
Collaborator

andrevidela commented Oct 30, 2024

Some places where code is elaborated the file context is a bit strange, it's probably hiding a bug or at least not explaining itself properly.

TTImp/ProcessDef.idr

       processType eopts nest env fc top Public []
          $ MkImpTy fc fc n $ holeyType (map snd args)
          -- Why does the name have the same location as the rest
          -- of the entire expression? That seems incorrect
          $ MkImpTy fc (MkFCVal fc n) $ holeyType (map snd args)

Idris/Elab/Interface.idr

Elaborated clauses inheriting a strange location

         let fnclause = PatClause vfc
                                  (INamedApp vfc
                                             -- Another suspicious location
                                             -- why do we take the location of the signature
                                             -- rather than the location of the name?
                                             (IVar sig.location cn.val)
                                             (UN $ Basic "__con")
                                             conapp
                                             )

Idris/Syntax.idr

Record field name locations are not tracked

 record RecordField' (nm : Type) where
    constructor MkRecordField
    doc : String
    rig : RigCount
    piInfo : PiInfo (PTerm' nm)
    names : List Name -- Those names should be `WithFC`
    type : PTerm' nm

TTImp/Elab/Case

guessScrType

the location of tyn is overriden with the location of the original name

                     applyTo defs (IVar (MkFCVal n.fc tyn)) tyty

updateClause

The location of cases inherit the locationof the clauses

              lhs' = apply (IVar $ MkFCVal loc' casen) args' in

TTImp/PartialEval

in mkRHSargs a lot of names inherit the location of the application node, rather than use their own

181|        = mkRHSargs ty (IApp fc app (IVar $ MkFCVal fc (UN $ Basic a))) as ds

TTImp/WithClause

hdLoc is used to give location to names but maybe they shouldn't since the location seems to span a much larger area than the name

TTImp/BindImplicits

bindUsings

in bindUsings, no location for pi name:

    = IPi (getFC ty) rig p (map NoFC mn) ty (bindUsings us tm)

piBind in piBindNames

no location used for pi name

205|       = IPi loc erased Implicit (Just (NoFC $ UN $ Basic n)) (Implicit loc False)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant