I was taken aback this was accepted

type Silly a b = Maybe b

x :: Silly Int Bool
x = Just True
y :: Silly Char Bool
y = Just False

z = x == y                    -- returns False

What's with the a in Silly's decl? That's not a phantom type. It's ignored and thrown away. So x and y are the same type, and can be compare for equality.

I expected a rule: all tyvars in the type's head must appear on rhs. Or at least a warning there was something silly. I tried -Wall, -fwarn-unused-binds, -Wunused-type-patterns.

I was just checking up on a remark that type synonyms are at the type level like implicit bidirectional pattern synonyms. For those, all vars must appear on both sides.