[ fix ] Process PiInfo in convert and unify

[spcfox]

Description

Now convert and unify do not compare PiInfo. As a result, the following code compiles successfully:

data X : Type -> Type

data X : Type => Type where

plus : Int -> {n : Int} -> Int
plus = (+)

This PR adds PiInfo processing to both functions. Also, due to unification, it allows resolve metavariables in default values (see DefaultHole.idr).

In additional to this, I changed AlreadyDefined to CantConvert when data is declared and defined with different types.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).