`sum-types`: Error more eagerly when a definition's name shadows an enum/newtype constructor

[RyanGlScott]

Surprisingly, Cryptol accepts this program on the sum-types branch (#1602):

newtype T a = { unT : a }

T = ()

It probably shouldn't. Cryptol will error if you actually try to use T anywhere, but Cryptol arguably should error as soon as you try to load the file.

Cryptol does eagerly error if you load this program using Cryptol 3.0.0 or the master branch:

$ ~/Software/cryptol-3.0.0/bin/cryptol Foo.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
[error]
    Overlapping symbols defined:
    (at Foo.cry:1:9--1:12, Main::T)
    (at Foo.cry:3:1--3:2, Main::T)
Loading module Cryptol

This suggests that there is an issue on the sum-types branch specifically.

The same issue also applies if T is an enum constructor.

[RyanGlScott]

I think the issue arises because the first T lives in the NSValue namespace while the second T lives in the NSConstructor namespace, and the overlapping-symbols check mistakenly concludes that the two symbols are distinct as a result. Compare the NamingEnv right before the overlapping-symbols check on the master branch:

NamingEnv (fromList [(NSValue,fromList [(UnQual (Ident False NormalName "T"),Ambig (fromList [Name {nUnique = 4670, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 9}, to = Position {line = 1, col = 12}, source = "Foo.cry"}},Name {nUnique = 4671, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 3, col = 1}, to = Position {line = 3, col = 2}, source = "Foo.cry"}}]))]),(NSType,fromList [(UnQual (Ident False NormalName "T"),One (Name {nUnique = 4669, nInfo = GlobalName UserName (OrigName {ogNamespace = NSType, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 9}, to = Position {line = 1, col = 12}, source = "Foo.cry"}}))])])

To the same NamingEnv on the sum-types branch:

NamingEnv (fromList [(NSValue,fromList [(UnQual (Ident False NormalName "T"),One (Name {nUnique = 4671, nInfo = GlobalName UserName (OrigName {ogNamespace = NSValue, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 3, col = 1}, to = Position {line = 3, col = 2}, source = "Foo.cry"}}))]),(NSConstructor,fromList [(UnQual (Ident False NormalName "T"),One (Name {nUnique = 4670, nInfo = GlobalName UserName (OrigName {ogNamespace = NSConstructor, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 9}, to = Position {line = 1, col = 12}, source = "Foo.cry"}}))]),(NSType,fromList [(UnQual (Ident False NormalName "T"),One (Name {nUnique = 4669, nInfo = GlobalName UserName (OrigName {ogNamespace = NSType, ogModule = TopModule (ModName "Main" NormalName), ogSource = FromDefinition, ogName = Ident False NormalName "T", ogFromParam = Nothing}), nFixity = Nothing, nLoc = Range {from = Position {line = 1, col = 9}, to = Position {line = 1, col = 12}, source = "Foo.cry"}}))])])

[RyanGlScott]

This might be a consequence of how the Semigroup instance for Names is implemented:

cryptol/src/Cryptol/ModuleSystem/Names.hs

Lines 28 to 36 in c00c9e5

	instance Semigroup Names where
	xs <> ys =
	case (xs,ys) of
	(One x, One y)
	| x == y -> One x
	| otherwise -> Ambig $! Set.fromList [x,y]
	(One x, Ambig as) -> Ambig $! Set.insert x as
	(Ambig as, One x) -> Ambig $! Set.insert x as
	(Ambig as, Ambig bs) -> Ambig $! Set.union as bs

This detects Ambiguity by using the Eq instance for Name, which in turn relies on the Eq instance for Namespace. The Eq instance for Namespace, however, distinguishes NSValue from NSConstructor, but we really shouldn't in this case. We should consider replacing the use of == here with a more coarse-grained equality function.

[RyanGlScott]

Then again, it's not quite as simple as replacing == with a different function, since the Set Name value used in the Ambig constructor relies on the Eq Name instance, which in turn relies on the behavior of == for Namespace. Perhaps we should define a newtype on top of Name with a different Eq instance and use it in Names?

[yav]

I wrote a function that moves the constructors to the value namespace before checking for ambiguities, which seems to solve the problem

[RyanGlScott]

Excellent, thanks! I've added some regression tests in 0c88cc3, so we can close this.