Pattern matching on unsaturated data constructors should be rejected

Currently the bogus equation unsatPatFunBindMaybe Just x = Just x gets the type forall {a1:Type}. forall {b1:Type}. Maybe a1 -> b1 -> Maybe b1, which is both completely wrong, and shouldn't be there in the first place.