Investigate suspicious cases of name parsing and processing

[spcfox]

Only simple UserName are parsed in binders, but more complex ones are allowed in some similar places. This leads to some strange behaviour. Examples:

Interface parameters

interface IfaceNS Name.Space.type where
  foo : Name.Space.type

IfaceNS Bool where
  foo = True

interface IfaceOp (<>) where
  bar : (<>)

IfaceOp Bool where
  bar = True

Data paremeters

data DataCaptaliseBool Bool = MkDataCaptaliseBool

foo : DataCaptaliseBool Bool
foo = MkDataCaptaliseBool

failing "Mismatch between: Type -> Type and Type"
  data DataCaptaliseList List = MkDataCaptaliseList

failing "Undefined name Name.Space.type"
  data DataNS Name.Space.type = MkDataNS

failing "Mismatch between: ?ty -> ?ty -> ?ty and Type"
  data DataOp (+) = MkDataOp

But in binders, capitalised names are allowed and namespaces and operators are forbidden:

data DataCaptalise : (List : Type) -> Type where
  MkDataCaptalise : DataCaptalise a

Record fields

record X where
  Name.Space.field : Type

foo : X -> Type
foo x = x.field

Main> :t field
Main.X.field : X -> Type