It’s often helpful to think about types in terms of the sets of possible runtime objects a type represents.
The Just[int] type is supposed to represent “all instances of the int type, but no instance of any subclass of int, including instances of bool.”
This means that the type int must not be assignable to the type Just[int], because the type int is a wider type (includes more objects). That’s the source of the unsoundness shown by @MegaIng above; the line value: Just[int] = arg (where arg: int) should be a type error, but it is not.
If Just[int] were a consistent/sound implementation of an exact integer type, the only things you could assign to a variable typed as Just[int] (or pass to a parameter typed as Just[int]) would be other expressions also typed as Just[int], and integer literals. This is what @mikeshardmind meant above about an exact type “requiring everyone to use it everywhere.”