Opened 5 years ago

Last modified 15 months ago

#9918 new bug

GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family

Reported by: qnikst Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: TypeFamilies, Instances Cc: goldfire, oleg
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

We hoped that closed type families could replace overlapping instances. It is not currently the case: GHC can resolve overlapping instances but cannot resolve the similar closed type family.

I'm attaching a minimized example of program where it can be observed. This is reproducible on ghc-7.8.3 and HEAD.

Attachments (2)

Minimal.hs (2.9 KB) - added by qnikst 5 years ago.
Miminized example.
Minimal.2.hs (2.0 KB) - added by qnikst 5 years ago.
Better minimized example

Download all attachments as: .zip

Change History (25)

Changed 5 years ago by qnikst

Attachment: Minimal.hs added

Miminized example.

comment:1 Changed 5 years ago 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

Changed 5 years ago by qnikst

Attachment: Minimal.2.hs added

Better minimized example

comment:2 Changed 5 years ago by qnikst

Sorry. Yes I can describe better.

What we are trying to do:

I have a code that uses monadic regions IORT and I want to write a function that allow to use a values from parent regions inside it's children shPutStrLn. In order to do it I need to write a type class class (Monad m1, Monad m2) => MonadRaise m1 m2 where lifts :: m1 a -> m2 a that allow me to lift actions from one monad to another.

One solution is to use Overlapping instances (lines 44-51) and it works perfectly.

Changes:

The idea was to provide a solution that doesn't require OverlappingInstances and uses closed type families to implement MonadRaise instead, lines 22-39.

The idea was to provide a type family TEQ that describes an equality* between monad stacks. equality* - is because we constraint the form of stacks a bit. Instead of having 2 Overlapping instances now we have one that calls a method from no-longer overlapping instance MonadRaise' and provides a proxy that is an evidence of our equality*.

It worked for all but one tests in our suite. The problem here is that MonadRaise' instance can't be deduced now (with or without adding explicit type signature to the test method):

Minimal.hs:58:12:
    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’

Why I think it should work:

I think that it could be possible to deduce MonadRaise' instance because TEQ (IORT s' m') (IORT s (IORT s' m') is False due to expression on line 24. and we have corresponding instance:

instance (Monad m2, m2 ~ (IORT s m2'), MonadRaise m1 m2') => MonadRaise' False m1 m2 where line 37.

As a result it seems that compiler have all information for selecting an instance of MonadRaise' False m1 m2 and thus MonadRaise m1 m2.

comment:3 Changed 5 years ago by simonpj

Cc: goldfire added

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 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

comment:4 Changed 5 years ago by goldfire

I agree with Simon's analysis.

The fact that thinking about infinite types means closed type families are less useful in more prosaic situations is annoying. But I don't know a way around this.

About Simon's interesting point (2): Some testing that I've done has made me even more confused, because I can't seem to witness the inconsistency. Are you sure that OverlappingInstances works here, even to select the MonadRaise m m instance? In my example, I was unable to get GHC to commit to the tyvars-equal instance without IncoherentInstances -- behavior I agree with. (It would destroy the type system to allow IncoherentInstances-like behavior with closed type families!)

I will say that your technique of using closed type families to produce some switch to control instance selection to avoid overlapping instances is a good way to do this. Of course, instance chains would be better -- which, of course, are just like closed type families for class instances. Since we don't have instance chains, you're doing the next-best thing, in my opinion.

My bottom line: I'm a little confused here, too. I believe that if GHC treats overlapping instances without the infinite-type reasoning, it would be possible to squeeze out proper incoherence among instances even without IncoherentInstances. But I couldn't seem to get it to happen!

comment:5 Changed 5 years ago 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.

comment:6 Changed 5 years ago by qnikst

I read the article and see a reasoning behind this solution, also I don't have an ideas or wishes about what solution will be right one.

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

I was a region code by Kiselev et al. And me and Oleg decided to give closed type families try to remove overloaded instances in the code. There are few other approaches that I have found like expressing type of the monadic stack as a typelevel list of monadic stacks then then check only relevant parts of that list, or calculate list length.

type family Listify (a :: * -> *) :: [* -> *] where
   Listify (IORT s m)  = IORT s m ': Listify m
   Listify m          = '[m]

Either of this approaches partially fix the issue, i.e. the code will work for statically known stack, for example:

test_copy = runSIO $ do
  hout <- newSHandle
  newRgn $  shPutStrLn hout

runSIO :: (forall s. IORT s IO v) -> IO v
runSIO = newRgn

But this approach do not allow to write region polymorphic code, as in all the cases I'm facing a case there type family can no longer be reduced as in all cases I'm finishing with something like:

MyTypeFamily (Listify m) (IORT s m, Listify m) and at this point it's not possible to make a right choice.

comment:7 Changed 5 years ago 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.

comment:8 Changed 5 years ago by oleg

Cc: oleg added

comment:9 Changed 5 years ago 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).

comment:10 Changed 5 years ago by simonpj

I conclude from this thread that

  • OverlappingInstances should probably obey the same rules as closed type families, for consistency.
  • But then both Oleg's versions would be rejected
  • "A foolish consistency is the hobgoblin of little minds". But there is a reason for the consistency, namely that we know that type inference might become unpredictable (i.e. succeed on Tuesday but fail on Friday, because of some difference in the order in which the solver solves constraints) if we allowed the more flexible form.
  • We don't yet know if there is any way to accept the programs Oleg wants (or something like them) without allowing unpredictability to slip in too.

I suppose that we could lift the restriction (ie strengthen the "surely-apart" check) if some flag is set:

  • 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 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'd like to work this out; the inconsistency between overlappping instances and type families is troubling.

Simon

comment:11 in reply to:  10 Changed 5 years ago by qnikst

Replying to 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.

comment:12 Changed 5 years ago by simonpj

OK. Let's see what Richard and Oleg think.

comment:13 in reply to:  10 Changed 5 years ago by goldfire

Replying to 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-apart" check) if some flag is set:

  • 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 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.

comment:14 Changed 5 years ago by qnikst

Seems I understood Simon differently. As far as I understood he advices make check for classes more strict, and less strict. So

  1. For classes instances:
instance F a (M a) where ...
instance F a a where ...

Will no longer be accepted due to surely-apart check. And Equals typefamily will have the same rules as it has now.

  1. As less programs will be accepted, and some really relies on the current behaviour, it's possible to introduce {-# UNDECIDABLE #-} pragma for type class that will remove new "surely-apart" check and instances will be accepted
  1. (Simon didn't say it). In order to unify type families and type class bevaiour it's possible to allow {-# UNDECIDANBLE #-} pragma to be applied to type family. Yes, if it will be applied to a typefamily that should have surely-apart check (e.g. Equals) it will be broken. However if programmer takes responsibility and guarantee that this check is not needed (2 examples above) then

he can use this pragma in order to make compiler accept this program.

So as far as I understood this suggestion doesn't allow any new ill-typed program to be accepted, more over some programs that are accepted now will not be accepted then, but proposal provides a backdoor so programmer can have old behaviour.

comment:15 Changed 5 years ago 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 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!

comment:16 in reply to:  15 Changed 5 years ago by goldfire

Replying to 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.

This seems to be precisely my {-# UNSAFE_STRONGER_APARTNESS_CHECK #-} pragma. Declaring this property of a type function seems orthogonal to whether or not evaluating the function terminates -- I could see both {-# UNDECIDABLE #-} and {-# UNSAFE_STRONGER_APARTNESS_CHECK #-} as separate pragmas, where neither implies the other. The first means that GHC might not terminate; the second means your program might not be type-safe.

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 Closed Type Families paper). But can you exhibit an example?

See #8162. That example uses open type families, and will compile and seg-fault with 7.6.3. The improved checking in 7.8.x stops compilation. However, an open type family with all of its instances in one module (such as F in #8162) is fully equivalent to a closed type family (with equations in any order). Why? Because all open type family instances must be compatible, and a closed type family where all the equations are compatible skips the apartness check during reduction. (See the closed type families paper for details.) Thus, if we did the wrong apartness check (that is, ignored the possibility of infinite types) in 7.8.x, then an example along the lines of #8162 would cause a seg-fault.

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!

I tried and failed at this, and I've decided it's impossible. Without using type families, classes introduce no new type axioms -- even with equality superclasses. Without any axioms, the proof of progress of FC is quite straightforward and has no surprises. Thus, any program with an implementation of unsafeCoerce must fail to be well-typed in FC. So, barring Core Lint errors, this trick shouldn't be possible.

So, I maintain my earlier position: what we have now is sound, but perhaps unpredictable in extreme cases. I do think we should make the class overlap check echo the type family overlap check, but I don't think there's a soundness issue here.

Last edited 5 years ago by simonpj (previous) (diff)

comment:17 Changed 5 years ago 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

comment:18 in reply to:  17 Changed 5 years ago by goldfire

Replying to simonpj:

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?

However, a mistake with type family reduction is unsound. A mistake with class instance selection is unpredictable/incoherent, but not unsound. I posit that we have such a mistake lurking here -- a loophole that, if we closed it, would prevent Oleg's working case from working.

comment:19 Changed 5 years ago 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.

comment:20 Changed 5 years ago by simonpj

GHC has always permitted types that are uninhabited (except by bottom); consider

data Void  -- No constructors

So I don't see why (undefined :: TT a) should be a problem. I certainly don't see a problem with test4 or test5. Your instance of C [a] does not require C a, and so of course we can compute the length of a list [TT a] without knowing anything about the type TT a. That's just parametricity.

Simon

comment:21 Changed 4 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:22 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:23 Changed 15 months ago by simonpj

Keywords: Instances added
Note: See TracTickets for help on using tickets.