#9082 closed bug (invalid)
Unexpected behavior involving closed type families and repeat occurrences of variables
Reported by: | haasn | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.2 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
Description
I'd expect both of these to work fine, but GHC always picks the instance that is mentioned first:
{-# LANGUAGE TypeFamilies, DataKinds #-} type family Bad a b where Bad (f a) a = False Bad a a = True bad :: ( Bad (f a) a ~ False , Bad a a ~ True ) => () bad = () -- Swapping the lines around does not change the behavior much: type family Bad' a b where Bad' a a = True Bad' (f a) a = False bad' :: ( Bad' (f a) a ~ False , Bad' a a ~ True ) => () bad' = () {- ctf.hs:7:8: Could not deduce (Bad a0 a0 ~ 'True) from the context (Bad (f a) a ~ 'False, Bad a a ~ 'True) bound by the type signature for bad :: (Bad (f a) a ~ 'False, Bad a a ~ 'True) => () at ctf.hs:(7,8)-(9,14) The type variable ‘a0’ is ambiguous In the ambiguity check for: forall (f :: * -> *) a. (Bad (f a) a ~ 'False, Bad a a ~ 'True) => () To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘bad’: bad :: (Bad (f a) a ~ False, Bad a a ~ True) => () ctf.hs:18:9: Could not deduce (Bad' (f0 a0) a0 ~ 'False) from the context (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) bound by the type signature for bad' :: (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) => () at ctf.hs:(18,9)-(20,14) The type variables ‘f0’, ‘a0’ are ambiguous In the ambiguity check for: forall (f :: * -> *) a. (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) => () To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘bad'’: bad' :: (Bad' (f a) a ~ False, Bad' a a ~ True) => () -}
Trying to turn this into an open type family instead somewhat hints at the issue:
type family Bad'' a b :: Bool type instance Bad'' a a = True type instance Bad'' (f a) a = False {- ctf.hs:58:15: Conflicting family instance declarations: Bad'' a a -- Defined at ctf.hs:58:15 Bad'' (f a) a -- Defined at ctf.hs:59:15 -}
It seems like GHC thinks these two family definitions conflict, yet to me they seem distinct - as a type that would match both would imply f a ~ a and hence be infinite.
Can anybody offer insight into this issue?
Change History (5)
comment:1 Changed 11 months ago by haasn
comment:2 Changed 11 months ago by haasn
Here's an updated example that fails. It seems the issue is more complicated, GHC picks the right case in the latter examples (regardless of order), but it fails on either ‘bar’ or ‘foo’ depending on the order of the cases in the type family Bad.
{-# LANGUAGE TypeFamilies, DataKinds #-} type family Bad a b where Bad (m a -> b) a = b Bad (a -> b) a = b foo :: Monad m => (m a -> b) -> a -> Bad (m a -> b) a foo f a = f (return a) bar :: (a -> b) -> a -> Bad (a -> b) a bar f a = f a {- ctf.hs:11:11: Couldn't match expected type ‘Bad (a -> b) a’ with actual type ‘b’ ‘b’ is a rigid type variable bound by the type signature for bar :: (a -> b) -> a -> Bad (a -> b) a at ctf.hs:10:8 Relevant bindings include a :: a (bound at ctf.hs:11:7) f :: a -> b (bound at ctf.hs:11:5) bar :: (a -> b) -> a -> Bad (a -> b) a (bound at ctf.hs:11:1) In the expression: f a In an equation for ‘bar’: bar f a = f a Failed, modules loaded: none. -} -- But this type-checks just fine: type family Bad' a b where Bad' (m a -> b) a = True Bad' (a -> b) a = False foo' :: (Monad m, Bad' (m a -> b) a ~ True) => (m a -> b) -> a -> b foo' f a = f (return a) bar' :: Bad' (a -> b) a ~ False => (a -> b) -> a -> b bar' f a = f a
comment:3 Changed 11 months ago by goldfire
- Resolution set to invalid
- Status changed from new to closed
As far as I can tell, GHC is doing the right thing here, but "the right thing" is subtle, indeed. We're at the intersection of closed type families, non-linear patterns, and infinite types, and that is a strange place indeed. I encourage you to read Section 6 of the closed type families paper. I will try to apply the logic there to your situation.
Let's focus on your first (simpler) example, as I think the reasoning there extends to the more complicated one in your most recent comment:
type family Bad a b where Bad (f a) a = False Bad a a = True
Now, consider the following beast:
type family G a where G a = Maybe (G a)
How can we reduce the target Bad (G Int) (G Int)? The first equation doesn't seem to match, and the second does. But, now we must do the apartness check with the first equation... is it ever possible for the first one to match? Sure it is, if the first (G Int) steps to (Maybe (G Int)) (with f |-> Maybe and a |-> G Int). So, the first equation isn't apart from our target, so the second equation can't be used. Perhaps GHC will be clever enough to reduce the first (G Int) and then apply the first equation, but I wouldn't hold my breath.
How does this affect you, without such a G? If we try to reduce a target Bad x x, GHC will be stuck. The first equation clearly doesn't match, and the second equation does. But, the first equation is not apart from Bad x x, because of the possibility that someone will define G and then instantiate x with G Int.
This case is subtle, and it took years of living with type families before we realized that this bizarre situation can actually cause a crash with open type families. See #8162. Though that bug deals with open families, I can imagine an adaptation that would cause a crash with closed ones.
An ideal world would produce an error report with a link to the paper, etc., in your situation, but detecting the situation is hard -- I believe we would have to run both the infinite unification algorithm as well as a normal unification algorithm, notice that the results are different, and then know we are in this place. I'm happy to see suggestions for a better way. If you do have suggestions, do please reopen. Or, perhaps it's worth putting in a feature request for a better error message, even without a way to achieve that goal.
comment:4 Changed 11 months ago by haasn
Thanks for the feedback.
As I understand it, G breaks this because it actually expands to an infinite type, and hence breaks my assumption that f a ~ a is impossible. This is also the reason why it requires UndecidableInstances.
However, it is also my understanding that this type of infinite type family expansion is actually undecidable, in that answering :k! Bad (G Int) (G Int) actually fails to terminate.
Do you know if there's an example of such a similarly ill-behaved G that either doesn't require UndecidableInstances or otherwise terminates with an incorrect result/breaks the type system if resolving Bad according to the reasoning outlined earlier?
As of now, I don't grok why this would be an actual problem. I'll probably have to look at the papers involved and also #8162 to answer this myself, but I thought I'd quickly ask here first.
comment:5 Changed 11 months ago by goldfire
I'm confident that any ill-behaved G would require UndecidableInstances. But, note that while that extension is needed in order to define G, it is not needed in order to use G. So, even if you do not have UndecidableInstances in your module, you are still under threat from such an attack.
Looking at the example in #8162, the problem would be exactly the same if the family F (the equivalent to your Bad) were a closed type family. Open type families LA and LB are used to expose the crash, but the family with the overlap could be made closed, as all of its instances are declared together. Note that F is defined without UndecidableInstances.
There is the possibility that some very clever analysis (and restrictions on things like G and/or UndecidableInstances) could allow Bad to behave as you might like. Indeed, we haven't actually proved type safety in the presence of non-linear (i.e., with a repeated variable on the LHS) and non-terminating type families, even taking infinite unification into account. That proof seems to require a solution to a recognized open problem. This lack of a proof actually extends to open type families as well -- the published proofs about non-terminating open type families implicitly (and very subtly) assumed linear patterns. After spending a Long Time working on this proof and failing to either find a proof or a counterexample, we (the authors of the "Closed Type Families" paper) were happy enough to conjecture type safety and keep non-linear patterns in the language.
All of this does add up to a slightly bumpy surface area for the closed type families feature. I'm quite aware of this and am somewhat disappointed about it. But, my thought is not to let the great become the enemy of the good here -- most uses of closed type families work in an intuitive way and are really helpful to people. Then, some uses work in a really unintuitive way, and people get confused. I still think it's a good trade-off.
Oh, while simplifying the example it seems I simplified too much, this bug goes away if you make ‘a’ and ‘b’ less ambiguous.
I'll have to think a bit more about the un-simplified example that fails to work, I may close this ticket again.