Importing instantiated submodule doesn't introduce members into scope.

[rybla]

#1363

When I run Lib2, I'm told Value not in scope: x. But it should be available from import submodule Lib1_Inst?

module Lib1 where
parameter
  type a : *
  x : a


module Lib2 where
parameter
  type b : *
  y : b

submodule Lib1_Inst = Lib1
  where
  type a = b
  x = y

import submodule Lib1_Inst
z : b
z = x

[yav]

Module Lib1 does not define anything, so when you import its instances Lib1_Inst you don't get anything in scope.

Perhaps the desugaring of Lib1 would help:

interface module S where
  type a : *
  x : a

module Lib1 where
  import interface S

Basically I think of module parameters as extra values that you have in scope, but they are not definitions in the module. of course, you could add extra definitions that are simply defined as the parameter, which would kind of mimic "exporting" a parameter.

[rybla]

Ok, yeah I misunderstood how parameters work. They "disappear" when you instantiate the functor; they aren't additional definitions that are exported.