[GHC] #9082: Unexpected behavior involving closed type families and repeat occurrences of variables
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by haasn): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: 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 [http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms.pdf 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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 [http://www.win.tue.nl/rtaloop/problems/79.html 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC