#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Can you be more explicit? * What, precisely, are the changes needed to do from "version that does work using overlapping instances" to "version that does not work using closed type families"? * What, as precisely as possible, does not work? * Why did you think it should work? I can't figure that out from the 50 lines of code you give. Thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: Aha. What I see is {{{ T9918.hs:64:32: Could not deduce (MonadRaise' (TEQ (IORT s' m') (IORT s (IORT s' m'))) (IORT s' m') (IORT s (IORT s' m'))) arising from a use of ‘shPutStrLn’ from the context (RMonadIO m') bound by the inferred type of test_copy :: RMonadIO m' => t -> FilePath -> IORT s' m' () at T9918.hs:(60,1)-(64,49) In the second argument of ‘(>>=)’, namely ‘shPutStrLn hout’ In the second argument of ‘till’, namely ‘(return "foo" >>= shPutStrLn hout)’ In a stmt of a 'do' block: till (return True) (return "foo" >>= shPutStrLn hout) }}} You are wondering why the first argument to `MonadRaise'`, namely `(TEQ (IORT s' m') (IORT s (IORT s' m')))`, doesn't reduce to `False`. Answer, because the first equation `TEQ m m` is not "surely apart" from `TEQ (IORT s' m') (IORT s (IORT s' m'))`. You may say that to make the first equation for `TEQ` succeed, we would need `m' = IORT s' m'`, which could only happen for infinite types. But, as you'll see from [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/ our closed type-families paper], we found that we had to use a slightly more conservative check, one that allows infinite types, for the surely-apart check. Why doesn't the same thing happen for overlapping type-classes; here GHC does decide that the two type can't be equal (because of the occurs check) and so picks the second commented-out instance, for `MonadRaise m1 m2`. So there are some interesting things here * Your program depends in a very delicate way on the treatment of infinite types. I wonder if it needs to? * Closed type families and type classes are treated differently. That seems inconsistent. In this particular example, I'm not sure which is "right". I'm adding Richard to cc because he may have a view. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by qnikst): Thanks for replies.

Your program depends in a very delicate way on the treatment of infinite types. I wonder if it needs to?

I need to think more about this, at this moment if was the most obvious way how to write required instances, but possibly there are more ways around.

Are you sure that OverlappingInstances works here, even to select the MonadRaise m m instance?

I've just checked the minimal example and I need to say that it doesn't choose `MonadRaise m m`, without explicit type signature: {{{ test_2 = do hout <- newSHandle shPutStrLn hout }}} however adding `test_2 :: IORT s IO ()` helps, in case of type families adding explicit type signature didn't help me in my experiments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by oleg): Perhaps the following two examples, deliberately simple, better illustrate the problem -- the difference in behavior of overlapping instances and closed type families. Example1: {{{ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE UndecidableInstances, OverlappingInstances #-} {-# LANGUAGE TypeFamilies #-} module Sub where data Z = Z data S n = S n -- x is greater than y by some amount class Sub x y where how_larger_is_x_than_y :: x -> y -> Int instance Sub x x where how_larger_is_x_than_y _ _ = 0 instance (x ~ (S x1), Sub x1 y) => Sub x y where how_larger_is_x_than_y ~(S x) y = 1 + how_larger_is_x_than_y x y -- The inferred type shows no constraints! So we obtained the result -- without instantiating the type of y, hence maintaining polymorphism. test y = how_larger_is_x_than_y (S (S y)) y -- inferred type: -- test :: x1 -> Int main = test (S Z) -- 2 }}} Example 2: rewritten using type families. This is how we hoped closed type families could eliminate overlapping instances. {{{ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} module Sub1 where data Z = Z data S n = S n class Nat a where nat :: a -> Int instance Nat Z where nat _ = 0 instance Nat n => Nat (S n) where nat ~(S n) = 1 + nat n type family Sub x y :: * where Sub x x = Z Sub (S x) y = S (Sub x y) how_larger_is_x_than_y :: forall x y. (Nat (Sub x y)) => x -> y -> Int how_larger_is_x_than_y x y = nat (undefined :: Sub x y) -- The inferred type has the unresolved constraint test y = how_larger_is_x_than_y (S (S y)) y -- test :: Nat (Sub (S (S y)) y) => y -> Int main = test (S Z) -- 2 }}} As you can see, with overlapping instances, GHC was able to eliminate the constraints on test. But with closed type families, it could not. There are no incoherent instances here, btw. In this simple example, the fact that test in the second example is no longer fully polymorphic does not matter. The code works anyway. But it does matter in the original (submitted) example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Thanks for the examples in comment:7. The first example can show up the very problem I was looking for! Consider this alternate ending to the first example there (which also needs `ScopedTypeVariables`): {{{ type family Inf x where Inf () = S (Inf ()) -- pattern-match on () avoids an eager occurs- check test2 (_ :: x) = test (undefined :: Inf x) -- test2 :: x -> Int main = test2 () }}} This will, of course, evaluate to `2`. But it arguably shouldn't, because `main` boils down to a comparison between `S (S (Inf ()))` and `Inf ()`, which is impossible to determine. The extra constraint that appears in the second example (the one with closed type families) essentially says that the two type-level numbers have a well-defined relationship. When infinity is involved, they don't, giving more reliable behavior (in extreme, perverse circumstances, admittedly). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by qnikst): Replying to [comment:10 simonpj]: Taking into account that this undecidability is used for purpose in number of libraries, (regions and hlists first comes into my mind, but there should be others) it worth to have a way to have this undecidability even in case if strenghtened "surely- apart" check will be used by default. And definitely this change will introduce some level of breakage in libraries. If "sulery-apart" check will be strengthened then `{-# UNDECIDABLE Foo #-}` solution looks very nice. And of cause per-type-family it looks much better (in the same sense as `XOverlappingInstances` that were deprecated in favor of `{-# OVERLAPPABLE #-}` pragma). And as far as I understand then in order to reach consistency it should be possible to use this pragma with closed type families and as a result first program will be accepted? In this case solution will be very good for me, as it will have a consistency by default and allow to switch from OverlappingInstances to closed type families in our case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:10 simonpj]:

I conclude from this thread that * `OverlappingInstances` should probably obey the same rules as closed type families, for consistency.

Generally agreed here, with the same reservations that Simon writes.

I suppose that we could lift the restriction (ie strengthen the "surely-

* I believe that the unpredictability only strikes if you have infinite types, via a looping type family. And a programmer might well be willing to guaranteed that will not occur. * In that sense, it's a bit like `-XUndecidableInstances`: the

apart" check) if some flag is set: programmer takes responsibility.

* And, as such it should probably be a per-type-family (or per-closed- type-family) pragma, rather than a global flag. Maybe even `{-# UNDECIDABLE #-}`.

I'm not sure exactly what you mean here (mostly). The `{-# UNDECIDABLE #-}` route is almost surely a good idea, independent of anything else, as it follows the new pattern started by `{-# OVERLAPPABLE #-}` and friends. But, critically, a dangerous use of a strengthened apartness check would happen on a family '''without''' this pragma. For example: {{{ type family Equals a b where Equals a a = True Equals a b = False }}} This clearly has no loops and should compile without `{-# UNDECIDABLE #-}`. Yet, if we use the strengthened apartness check when choosing to reduce by the second equation, we can get into trouble. Specifically, should `Equals x [x]` reduce to `False`, for some skolem `x`? If, in some future module, we introduce `type family Loop where Loop = [Loop]`, then it would be terrible to have reduced `Equals x [x]` to `False`. But, of course, we have no way of knowing if `Loop` will come into being in the future. The nub of the problem, as I see it, is that the safety (for closed type families) or predictability (for class instances) of the system depends on some '''global''' no-looping property. I could see some `{-# UNSAFE_STRONGER_APARTNESS_CHECK #-}` pragma that could be put on `Equals` that would enable the stronger check and let the programmer bear the safety burden. However, this is a significant departure from other "let the programmer beware" issues in that, for closed type families, you can abuse this ability to implement `unsafeCoerce`. (This would not be the case for class instances.) So, getting back to Simon's proposal: what's your suggested behavior? I see what you want with `{-# UNDECIDABLE #-}`, but I don't see precisely how it would influence the apartness check. If we are going to start treating undecidable instances as different than regular ones, it would be worthwhile to make the termination checker smarter. Right now, a standard Peano multiplication type family requires `-XUndecidableInstances`. I think the assumed safety of that extension (I think folks are OK with a perhaps-looping compiler, as long as the produced binary, if any, is type-safe) allows people to use it without much hesitation, so there has been little (no?) pressure to improve the termination checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): The straw-man proposal is that with `{-# UNDECIDABLE #-}` (or some other pragma name) on a closed type family, the surely-apart check is strengthened, allowing more reductions to fire. Richard, you rightly point out that if you put that on `Equal`, then `Equal x [x]` would return `False`, as you'd expect if all types were finite. But you also claim that if you can define an infinite type, then you can get `unsafeCoerce`. I believe you (c.f Section 6 of the [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/ Closed Type Families paper]). But can you exhibit an example? And if you can, can you translate it back into an example using overlapping classes, probably with equality superclasses? If so, perhaps our existing compiler is unsound! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): I feel stuck on this. I can see Oleg's goal, but I don't want to require him to use a potentially-unsound route to gain it. It's tantalising that overlapping type classes achieve the same end without risking unsoundness. Surely we must be able to replicate this in type families, somehow? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by oleg): I too have tried to induce unsoundness with overlapping instances and concluded it is unlikely -- although there is plenty of strange and incoherent behavior one can observe. The straightforward attempt to pack an existential in one type class environment and unpack it in another module (where a more specialized instance is introduced) does not work because the existential is packed with the corresponding dictionary. When it is unpacked, the packed dictionary is used -- regardless how many new instances become available. Without type families, a type variable always stood for some ground type, at least potentially. When we assert a constraint C a on the type variable a, that constraint will not be dropped or discarded. It will be explicitly passed around, until it is resolved (or cannot be resolved -- in which case an error is reported). That is why it is safe to do instance selection for unground types: if we have {{{ class C a where foo :: a -> Int instance C [a] where foo = length test3 x = foo [x] }}} the inferred type for test3 :: t -> Int has no constraints. We resolved C [t] for the unground type t. If t had other constraints, they will be preserved. With type functions, we are no longer sure what the type variable represents. It can be a non-reduced type-function application. So a type variable now stands not for a value (ground type) but for an expression. And that could be a problem. For example: {{{ type family TT a -- no instances newtype D a = D{unD:: [TT a]} test4 (x::a) = foo (unD (undefined:: D a)) test5 (x::a) = foo (unD (D []:: D a)) }}} The code type-checks and test5 () even runs, returning 0. So, although T a has no instances, we have successfully ignored that fact. That trick would not have worked with only type classes; if we add a constraint we can't cast it away, and the type checker will demand sooner or later the constraint be satisfied. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: TypeFamilies, Resolution: | Instances Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, Instances -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler