{"action":"created","issue":{"url":"https://api.github.com/repos/ekmett/constraints/issues/12","labels_url":"https://api.github.com/repos/ekmett/constraints/issues/12/labels{/name}","comments_url":"https://api.github.com/repos/ekmett/constraints/issues/12/comments","events_url":"https://api.github.com/repos/ekmett/constraints/issues/12/events","html_url":"https://github.com/ekmett/constraints/issues/12","id":109842093,"number":12,"title":"Bottom seems insufficiently general to be useful","user":{"login":"treeowl","id":1893117,"avatar_url":"https://avatars.githubusercontent.com/u/1893117?v=3","gravatar_id":"","url":"https://api.github.com/users/treeowl","html_url":"https://github.com/treeowl","followers_url":"https://api.github.com/users/treeowl/followers","following_url":"https://api.github.com/users/treeowl/following{/other_user}","gists_url":"https://api.github.com/users/treeowl/gists{/gist_id}","starred_url":"https://api.github.com/users/treeowl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/treeowl/subscriptions","organizations_url":"https://api.github.com/users/treeowl/orgs","repos_url":"https://api.github.com/users/treeowl/repos","events_url":"https://api.github.com/users/treeowl/events{/privacy}","received_events_url":"https://api.github.com/users/treeowl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-10-05T17:01:37Z","updated_at":"2015-11-13T02:28:10Z","closed_at":null,"body":"`bottom` demonstrates that a particular unsatisfiable constraint, `() ~ Bool`, entails any constraint. This is not a particularly interesting false constraint, and there doesn't *seem* to be any particularly obvious way to produce it from other false constraints. I don't have anything approaching a full solution, but here are some ideas to think about, based on the notion that if a constraint can prove void, it must be wrong:\r\n\r\n```haskell\r\ncrazy :: (c => Void) -> c :- d\r\ncrazy q = Sub (absurd q)\r\n```\r\n\r\nFrom this, we can recover the `() ~ Bool` idea in a way that can be used much more generally.\r\n\r\n```haskell\r\n-- Proof that one type doesn't unify with another\r\nnewtype (/=) a b = NE {no :: forall c . (a :~: b) -> c}\r\n\r\n-- If two types don't unify, then the assumption that they do entails anything.\r\nhola :: forall a b d . a /= b -> (a ~ b) :- d\r\nhola (NE nope) = crazy $ nope (Refl :: a :~: b)\r\n\r\n-- A type useful for proving inequality\r\ndata Yeah this that a where\r\n  Yeah1 :: Yeah this that this\r\n  Yeah2 :: (forall b . b) -> Yeah this that that\r\n\r\n-- Getting to Yeah\r\nhoop :: forall a b . (a :~: b) -> Yeah a b b\r\nhoop Refl = Yeah1\r\n\r\n-- The specific example of `() ~ Bool`, expressed concisely; to prove other inequations,\r\n-- only the type signature needs to be changed.\r\nhum :: () /= Bool\r\nhum = NE $ \\ab -> case hoop ab of Yeah2 x -> x\r\n```"},"comment":{"url":"https://api.github.com/repos/ekmett/constraints/issues/comments/156302246","html_url":"https://github.com/ekmett/constraints/issues/12#issuecomment-156302246","issue_url":"https://api.github.com/repos/ekmett/constraints/issues/12","id":156302246,"user":{"login":"treeowl","id":1893117,"avatar_url":"https://avatars.githubusercontent.com/u/1893117?v=3","gravatar_id":"","url":"https://api.github.com/users/treeowl","html_url":"https://github.com/treeowl","followers_url":"https://api.github.com/users/treeowl/followers","following_url":"https://api.github.com/users/treeowl/following{/other_user}","gists_url":"https://api.github.com/users/treeowl/gists{/gist_id}","starred_url":"https://api.github.com/users/treeowl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/treeowl/subscriptions","organizations_url":"https://api.github.com/users/treeowl/orgs","repos_url":"https://api.github.com/users/treeowl/repos","events_url":"https://api.github.com/users/treeowl/events{/privacy}","received_events_url":"https://api.github.com/users/treeowl/received_events","type":"User","site_admin":false},"created_at":"2015-11-13T02:28:10Z","updated_at":"2015-11-13T02:28:10Z","body":"These alternate bikeshed colors seem strictly less convenient, as we discussed. The first one is a triviality, so I see no value in it whatsoever. The second is perhaps more efficient, but it likely pushes the `absurd` application to the caller while making it a bit harder to see from the type what it's for."}}