Soundness issue around type families

[soundlogic2236]

The plugin's handling of type families is very strange and unsound. For one thing, it treats type families that output natural numbers as constant, which is obviously unsound:

type family Simple (n :: Bool) :: Nat where
    Simple 'False = 0
    Simple 'True = 1

invalid :: forall x y. Simple x :~: Simple y
invalid = Refl

And here is the (trivial) proof of unsoundness:

type family RevSimple (n :: Nat) :: Bool where
    RevSimple 0 = 'False
    RevSimple 1 = 'True

absurdity :: 'True :~: 'False
absurdity = applyRev $ invalid @'True @'False where
    applyRev :: forall x y. x :~: y -> RevSimple x :~: RevSimple y
    applyRev Refl = Refl

It appears to also equate even distinct type families, as long as they have the same number of arguments applied, even cases like:

type family Simple (n :: Bool) :: Nat where
    Simple 'False = 0
    Simple 'True = 1

type family Weird :: Nat -> Nat where

invalid :: forall x y. Simple x :~: Weird y
invalid = Refl

However, this doesn't work if y is replaced with a constant.

invalid :: forall x. Simple x :~: Weird 0
invalid = Refl

doesn't typecheck, and neither does:

invalid :: forall x y. Simple x :~: Weird (y + 1)
invalid = Refl

However, this does:

type family Simple (n :: Nat) :: Nat where
    Simple 0 = 0
    Simple 1 = 1

type family Weird :: Nat -> Nat where

invalid :: forall x y. Simple (x + 1) :~: Weird (y + 1)
invalid = Refl

[konn]

Thank you for reporting! That seems really a severe issue, too. I will try to investigate the issue as soon as possible.