I’m on a train, so can’t look at your code. But I urge you (or whoever) to split the task into two:
· Traverse the Core tree, gathering given constraints, deleting unreachable branches
· The Contradiction Checker (CCK)
CCK is independently useful; for example George et al may use it when traversing HsSyn to report overlapping patterns.
The API of CCK might look something like this:
contradictionCheck :: FamInstEnvs -> [PredType] -> [PredType] -> Bool
· FamInstEnvs tells it what type-family-instances exist
· The first [PredType] are the enclosing givens
· The second [PredType] are the givens of a new pattern match
· Result is True if the new pattern match is inaccessible
One might also consider a more incremental API, something like
data ContradictionChecker
newCCK :: FamInstEnvs -> ContradictionChecker
check :: ContradictionChecker -> [PredType] -> Maybe ContradictionChecker
Returns Nothing for a contradiction, (Just cc) if the branch is reachable, where you should use cc for the body of the branch.
I like the latter API. For example a ContrdictionChecker might carry a renaming of type variables, to account for shadowing.
Simon
From: conal.elliott@gmail.com [mailto:conal.elliott@gmail.com] On Behalf Of Conal Elliott
Sent: 25 June 2014 00:11
To: Simon Peyton Jones
Cc: Dimitrios Vytiniotis; ghc-devs@haskell.org; Nikolaos S. Papaspyrou (nickie@softlab.ntua.gr); George Karachalias
Subject: Re: Pruning GADT case alternatives with uninhabitable coercion parameters
I'm glad for the interest and help. I can make an initial go of it. My current simple plan is to traverse expressions, collecting type equalities from bound coercion variables as I descend, combining them progressively with successive type unifications. The traversal is thus parametrized by a TvSubst and yields a Maybe TvSubst. The coercion variables will come from lambdas, let bindings and case alternatives. If an added equality is not unifiable given the current TvSubst, we've reached a contradiction. If the contradiction arises for one of the variables in a case alternative, then remove that alternative.
How does this strategy sound?
Some issues:
* Nominal vs representational type equalities.
* Will I want to normalize the types (with normaliseType) before unifying?
* How can I unify while carrying along a type substitution environment? The Unify module exports tcUnifyTy, which takes no such environment, but not unify, which does.
-- Conal
On Tue, Jun 24, 2014 at 4:43 AM, Simon Peyton Jones
case ds of wild (Sum Int) L (~# :: S (S Z) ~N Z) a1 -> f a1 B n1 (~# :: S (S Z) ~N S n1) uv -> ...
Note the kind of the coercion parameter to the leaf constructor (`L`): `S (S Z) ~N Z`, i.e., 2 == 0. I think we can safely remove this branch as impossible. The reasoning gets subtler, however. After inlining and simplifying in the second (`B`) alternative, the following turns up:
case ds0 of wild0 (Sum Int) L (~# :: n1 ~N Z) a1 -> f0 a1 B n2 (~# :: n1 ~N S n2) uv0 -> ...
Now I want to remove the first `L` alternative with `n1 ~ Z`, given that the kind `S (S Z) ~N S n1` is inhabited (since we're in the first `B` alternative), so that `n1 ~ S Z`. With more inlining, more such equalities pile up. Soon we get to an impossible `B` alternative, whose removal would then eliminate the rest of the recursive unfolding. My questions: * Does this sort of transformation already live in GHC somewhere, and if so, where? * Are there gotchas / sources of unsoundness in the transformation I'm suggesting? * Is anyone else already working on this sort of transformation? -- Conal