Instances in local modules are automatically imported potentially causing unintended clashes

[lukaszcz]

This seems intuitive, but has some unintended consequences in combination with instance resolution.

Consider:

module instanceModule;

import Stdlib.Data.List.Base open;
import Stdlib.Trait.Show open;
import Stdlib.Data.String open;

module showModule;

showList {A} {{Show A}} : List A -> String
  | nil := "nil"
  | (h :: t) := Show.show h ++str " :: " ++str showList t;

instance
showListI {A} {{Show A}} : Show (List A) :=
   mkShow@{show := showList};

end;

showList' {A} {{Show A}} : List A -> String := Show.show;

This type-checks, because the after the definition of showModule it is automatically imported, which adds all instances declared inside the module to instance search. This makes it impossible to define a different instance for Show (List A) in another local module.

The following

module instanceModule;

import Stdlib.Data.List.Base open;
import Stdlib.Trait.Show open;
import Stdlib.Data.String open;

module showModule;

showList {A} {{Show A}} : List A -> String
  | nil := "nil"
  | (h :: t) := Show.show h ++str " :: " ++str showList t;

instance
showListI {A} {{Show A}} : Show (List A) :=
   mkShow@{show := showList};

end;

module showModule2;

instance
showListI {A} {{Show A}} : Show (List A) :=
   mkShow@{
     show : List A -> String
       | nil := "nil"
       | (h :: t) := Show.show h ++str " :: " ++str show t;
   };

end;

fails the type-checker with

/Users/heliax/Documents/progs/juvix/instanceModule.juvix:22:1-10: error:
The instance showListI is subsumed by instances at:
  • /Users/heliax/Documents/progs/juvix/instanceModule.juvix:14:1-10

I'm not sure how much of a problem this is in actual programs, but I did encounter this when trying to use modules to hide things when writing the documentation in Juvix markdown.