Typechecker confuses constants included from parametric theory and fails

[ComFreek]

@florian-rabe Can you have a look at this? @Jazzpirate said we would need your help for resolving this. Currently, this is a semi-blocking issue for FrameIT.

How to reproduce

MitM/core defines points and lines a modular way. It starts with the 3DGeometry theory

theory 3DGeometry =
  include ☞base:?ProductTypes ❙
  include ?Geometry ❙

  point = ℝ × ℝ × ℝ ❙
  [...]
  include (?Geometry/Common point point_addI point_subtractI vec_multI scalar_productI) ❙
  [...]

that in turn includes the parametric Geometry/Common theory:

theory Geometry =
  include ☞arith:?RealArithmetics ❙
  include ☞base:?Trigonometry ❙

  theory Common > point : type,
        add : point ⟶ point ⟶ point,
        subtract : point ⟶ point ⟶ point,
        mult : ℝ ⟶ point ⟶ point,
        scp : point ⟶ point ⟶ ℝ ❘ =

      [...]

      line_type : type ❘ # line ❙
      lineOf : point ⟶ point ⟶ line ❘ # from 1 to 2 ❙

With that setup the following fails to typecheck (e.g. in as seen in the Examples theory of our FrameIT/frameworld repository.)

theory Examples =
  A: point ❘ = ⟨1.0, 2.0, 3.0⟩❙
  B: point ❘ = ⟨4.0, 5.0, 6.0⟩❙

  // this doesn't typecheck due to an MMT bug ❙
  line_AB: line_type ❘ = lineOf A B ❙
❚

Error:

error while adding successfully parsed element http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB: variable point not declared in context http://mathhub.info/FrameIT/frameworld?ScrollMeta, http://mathhub.info/FrameIT/frameworld/examples?Examples

[ComFreek]

Example of non-reproducing sample (it typechecks fine):

namespace http://mathhub.info/FrameIT/frameworld/examples/bug-repro ❚

fixmeta ur:?LF ❚

theory Outer =
  theory Inner : ur:?LF > point : type ❘ =
    aline_type : type ❙
    alineOf: point ⟶ point ⟶ aline_type ❙
  ❚

  point: type ❙
  include (?Outer/Inner point) ❙

  A: point ❙
  B: point ❙
  sampleLine: aline_type ❘= alineOf A B ❙
❚