допустим у меня есть это
class Convertible initar supplement finit residue where
 transform :: initar -> supplement -> (finit, residue)

дальше я хочу сказать что два типа идентичны если их можно превратить один в другой без потери информации или необходимости добавлять информацию
class (forall a b . Convertible b () a (), Convertible a () b ())
  => Identical a b

Даьлше я хочу сказать что два типа обратимы если при конвертации из одного в лругой теряется информация, которая достаточна чтобы совершить обратное преобразование при условии что существует прообразование отстаток от которого достаточен чтобы превратить один тип в лругой
class (forall a b s t1 . Convertible a s b t1, Convertible b t1 a s)
  => HasTrivialInvertion a

Последнее не компилируется

А Identical должен именно идентичность в каком смысле показывать? Просто с вашим текущим определением можно тогда доказать, что List и Unit идентичны, например.

transform :: List -> Unit -> (Unit, Unit)
transform _ _ = (unit, unit)

transform :: Unit -> Unit -> (List, Unit)
transform _ _ = (nil, unit)

допустим у меня есть это
class Convertible initar supplement finit residue where
 transform :: initar -> supplement -> (finit, residue)

дальше я хочу сказать что два типа идентичны если их можно превратить один в другой без потери информации или необходимости добавлять информацию
class (forall a b . Convertible b () a (), Convertible a () b ())
  => Identical a b

Даьлше я хочу сказать что два типа обратимы если при конвертации из одного в лругой теряется информация, которая достаточна чтобы совершить обратное преобразование при условии что существует прообразование отстаток от которого достаточен чтобы превратить один тип в лругой
class (forall a b s t1 . Convertible a s b t1, Convertible b t1 a s)
  => HasTrivialInvertion a

Последнее не компилируется

Я так понял, условие "без потери информации" тут задаётся с помощью юнитов

допустим у меня есть это
class Convertible initar supplement finit residue where
 transform :: initar -> supplement -> (finit, residue)

дальше я хочу сказать что два типа идентичны если их можно превратить один в другой без потери информации или необходимости добавлять информацию
class (forall a b . Convertible b () a (), Convertible a () b ())
  => Identical a b

Даьлше я хочу сказать что два типа обратимы если при конвертации из одного в лругой теряется информация, которая достаточна чтобы совершить обратное преобразование при условии что существует прообразование отстаток от которого достаточен чтобы превратить один тип в лругой
class (forall a b s t1 . Convertible a s b t1, Convertible b t1 a s)
  => HasTrivialInvertion a

Последнее не компилируется

А уже обсудили что там Снойман удумал с векторными типами делать?