Constructors not accessible in the REPL about datatt HOT 2 CLOSED

Yes this is on purpose. Constructors can be overloaded/reused, so they can't have their type synthesized, only checked. Consider

data Unit => tt
data Bool => tt | ff
def x => tt

What type should x have? It's unclear. Instead you'd have to write

def x : Unit => tt

or

def x : Bool => tt

Agda actually does exactly the same thing, except it has a special case where the type of a constructor can be inferred if it appears in only one datatype declaration. This could be added, but I don't think it's a big deal.

from datatt.

Ah thanks, that explains it.

from datatt.