```agda none : Int [{} : Set X] none = [42] weak : forall {a : Type} . a [{} : SetOp X] -> () weak [_] = () good3 : () good3 = weak none ``` This type checks despite`none` being `Set` instead of `SetOp`.