I was reading an answer by Luis Casillas on Stack Overflow http://stackoverflow.com/a/23418746/1477667 and he used a somewhat peculiar type, with apparently not-so-useful constraints: newtype f :-> g = Natural { eta :: forall x. (Functor f, Functor g) => f x -> g x } There are a couple things about it that I don't understand. 1. I can construct a :-> from a function that doesn't satisfy the constraints, and I can pattern match to get access to it, but I can't use it. Why am I allowed to construct it at all? data Mb a = N | J a -- Not a Functor instance -- This is accepted (why?) pot = Natural (\case [] -> N (a:_) -> J a) -- And I can even do this: mb :: Functor Mb => Mb Int mb = case pot of Natural f -> f [3] But then of course I can't satisfy the constraint to use it. 2. I would have thought that such a weird/broken thing as this would only be allowed with -XDatatypeContexts, but in fact it is allowed without it. Why? David