idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

Investigate suspicious location tracking #3409

Open andrevidela opened 3 weeks ago

andrevidela commented 3 weeks ago

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)
andrevidela commented 2 days ago

Possibly related