Exhaustiveness-checking warning loses module namespace upon reload

[RyanGlScott]

Consider this program:

module GuardOrder where

parameter
  type w: #
  type w' = 2 ^^ w
  type b = 2 ^^ w'

f' : [b] -> [b]
f' x
  | b == 2 => ~ x
  | b > 2 => x
  | b < 2 => x

Currently, Cryptol deems f' to be inexhaustive (see #1796 for more on this, but this is a separate issue than what I am reporting here). If you load this module into Cryptol, then the warning is:

$ ~/Software/cryptol-3.2.0/bin/cryptol Bug.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0 (1bcb75c)
https://cryptol.net  :? for help

Loading module Cryptol
Loading interface module `parameter` interface of GuardOrder
Loading module GuardOrder
[warning] at Bug.cry:9:1--9:3:
  Could not prove that the constraint guards used in defining GuardOrder::f' were exhaustive.

Note that the warning message mentions GuardOrder::f', which includes the module namespace (as expected). So far, so good.

Now let's reload the program:

GuardOrder(parameterized)> :reload
Loading module Cryptol
Loading interface module `parameter` interface of GuardOrder
Loading module GuardOrder
[warning] at Bug.cry:9:1--9:3:
  Could not prove that the constraint guards used in defining f' were exhaustive.

This time, the warning mentions f', not GuardOrder::f'. Somehow, the module namespace disappeared in the process of reloading the program!

---

As a more extreme example, let's quit Cryptol:

GuardOrder(parameterized)> :quit

And invoke Cryptol on it again:

$ ~/Software/cryptol-3.2.0/bin/cryptol Bug.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0 (1bcb75c)
https://cryptol.net  :? for help

Loading module Cryptol
Loading interface module `parameter` interface of GuardOrder
Loading module GuardOrder
[warning] at Bug.cry:9:1--9:3:
  Could not prove that the constraint guards used in defining GuardOrder::f' were exhaustive.

Again, it mentions GuardOrder::f'—so far, so good. Now, without exiting the Cryptol REPL, let's modify the program to add another definition, which is also deemed inexhaustive:

module GuardOrder where

parameter
  type w: #
  type w' = 2 ^^ w
  type b = 2 ^^ w'

f' : [b] -> [b]
f' x
  | b == 2 => ~ x
  | b > 2 => x
  | b < 2 => x

// This definition is new
f'' : [b] -> [b]
f'' x
  | b == 2 => ~ x
  | b > 2 => x

If we reload the REPL now, we get:

GuardOrder(parameterized)> :reload
Loading module Cryptol
Loading interface module `parameter` interface of GuardOrder
Loading module GuardOrder
[warning] at Bug.cry:16:1--16:4:
  Could not prove that the constraint guards used in defining GuardOrder::f'' were exhaustive.
[warning] at Bug.cry:9:1--9:3:
  Could not prove that the constraint guards used in defining f' were exhaustive.

Note that the warning for the newly added definition mentions GuardOrder::f'', which does include a module namespace, but the warning for the old definition mentions f', which does not include a module namespace! Very strange indeed.

[yav]

The bug here is more likely that we do print the qualified names, rather that we don't. This all has to do with a system where we qualify names only when they are not in scope or ambiguous (I think it was based on GHC originally) but we are not very consistent about using it. Also, I think there are some cases where we don't know which scope we are talking about. Have a look in Utils.PP