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.

[lukaszcz]

Fortunately, we name instances, so we could provide syntax for hiding/using them, e.g.,

import Module1 using {instance showListI};

Then we wouldn't automatically import instances unless the module is opened. Maybe then we also need syntax to use / hide all instances:

import Module1 using instances;
import Module2 open hiding instances;

This would also provide a manual solution for clashes of orphan instances. The potential for clashes when importing different instances for the same type from two different modules is the reason why Haskell gives a warning for orphaned instances and Rust disallows them. With named instances, one could manually hide some of them to resolve a clash.