On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:
(Moving to ghc-users, there's nothing particularly dev-y.)
Sometimes it woulld be useful to be able to reason backwards about type families.
Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type families compared to FunDeps.
For example, we have
type family a && b where 'False && b = 'False 'True && b = b a && 'False = 'False a && 'True = a a && a = a
... if we know something about the *result*, GHC doesn't give us any way to learn anything about the arguments.
You can achieve the improvement you want today. You'll probably find Oleg has a solution With FunDeps and superclass constraints, it'll go like this class (OnResult r a b, OnResult r b a) => And a b r | a b -> r instance And 'False b 'False -- etc, as you'd expect following the tf equations -- the instances are overlapping but confluent class OnResult r a b | r a -> b instance OnResult 'True a 'True instance OnResult 'False 'True 'False You could equally make `OnResult` a type family. If you can trace backwards to where `&&` is used, you might be able to add suitable constraints there. So there's a couple of futures: * typechecker plugins, using an SMT solver * injective type families the next phase is supposed to allow type family a && b = r | r a -> b, r b -> a where ... That will help with some type families (such as addition of Nats), plug1 https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/propos... but I don't see it helping here. plug2 (this example) https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/propos... Because (for example) if you unify the first two equations, (that is, looking for coincident overlap) 'False && 'False = 'False 'True && 'False = 'False That's inconsistent on dependency ` r b -> a`. And you can't fix it by re-ordering the closed equations.
For (&&), the obvious things you'd want are ...
There's nothing inherently impossible about this sort of reasoning.
No-ish but. It relies on knowing kind `Bool` is closed. And GHC doesn't pay attention to that. So you need to bring type family `Not` into the reasoning; hence a SMT solver.
... I wouldn't necessarily expect GHC to be able to work something like this out on its own.
That's a relief ;-)
But it seems like there should be some way to allow the user to guide it to a proof.
Yes, an SMT solver with a model for kind `Bool`. (And a lot of hard work to teach it, by someone.) AntC