Opened 10 years ago

Last modified 9 months ago

#2256 new bug

Incompleteness of type inference: must quantify over implication constraints

Reported by: simonpj Owned by: simonpj
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 6.8.2
Keywords: Cc: Iceland_jack, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider this program (from Iavor)

f x = let g y = let h :: Eq c => c -> ()
                    h z = sig x y z
                in ()
      in fst x

sig :: Eq (f b c) => f () () -> b -> c -> ()
sig _ _ _ = ()

This example is rejected by both Hugs and GHC but I think that it is a well typed program. The Right Type to infer for g is this:

g :: forall b. (forall c. Eq c => Eq (b,c)) => b -> ()

but GHC never quantifies over implication constraints at the moment. As a result, type inference is incomplete (although in practice no one notices). I knew about this, but I don't think it's recorded in Trac, hence this ticket.

Following this example through also led me to notice a lurking bug: see "BUG WARNING" around line 715 of TcSimplify.

Change History (27)

comment:1 Changed 9 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:2 Changed 9 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:3 Changed 9 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:4 Changed 8 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:5 Changed 7 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:6 Changed 7 years ago by simonpj

Type of failure: None/Unknown

OK, with the new typechecker the BUG WARNING problem has gone away. However, when we are attempting to generalise a local binding (remember, this isn't recommended; I'd prefer to have -XMonoLocalBinds on), there is a fixable incompleteness in the algorithm. Specifically, suppose we are generalising a let-binding with constraints (Eq a, (forall b. Ord b => ...a...b....)), and we want to generalise over a. Then

  • When generalising, we call simplifyAsMuchAsPossible.
  • This in turn fails if it can't eliminate all implication constraints. So Iavor's example fails with
    T2256.hs:4:27:
        Could not deduce (Eq (f b c)) from the context (Eq c)
          arising from a use of `sig'
    
  • A slightly more generous plan would be

    • EITHER not to generalise over any variables mentioned in the implication, and float it. In the example, don't generalise over a after all.

    • OR to abstract over the quantified type variables constaints, and float that, in the hope that some later unification will render it soluble. In the example, generate the implication (forall a. Eq a => (forall b. Ord b => ...a...b...)).

I'm not sure which is better, and it's very obscure anyway, so I don't think it's high priority. I'm just making these notes while I think of them.

Simon

comment:7 Changed 7 years ago by igloo

Milestone: 7.0.17.0.2

comment:8 Changed 7 years ago by igloo

Milestone: 7.0.27.2.1

comment:9 Changed 6 years ago by igloo

Milestone: 7.2.17.4.1

comment:10 Changed 6 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lowlowest

comment:11 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:12 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:13 Changed 3 years ago by thomie

Component: CompilerCompiler (Type checker)
Type of failure: None/UnknownGHC rejects valid program

SPJ: this ticket is not listed on Status/SLPJ-Tickets.

The error message with HEAD (ghc-7.9.20141204):

    Could not deduce (Eq b) arising from a use of ‘sig’
    from the context (Eq c)
      bound by the type signature for h :: Eq c => c -> ()
      at test.hs:5:26-40
    Possible fix:
      add (Eq b) to the context of
        the type signature for h :: Eq c => c -> ()
        or the inferred type of g :: b -> ()
    In the expression: sig x y z
    In an equation for ‘h’: h z = sig x y z
    In the expression:
      let
        h :: Eq c => c -> ()
        h z = sig x y z
      in ()

comment:14 Changed 3 years ago by goldfire

I initially put this ticket into my internal notes as "Difficulty: Rocket Science", but I've changed my mind. I think this is actually straightforward to implement.

GHC already has implication constraints, except that they're effectively all Wanteds. So, all we would need are to be able to make Given implication constraints. But, these should be rather straightforward, because we can view top-level instances as Given implication constraints. We can just adapt the current look-in-Givens algorithm to do some matching, just like the instance-selection algorithm does. When we find an implication-constraint Given that matches a Wanted, we use it to solve the Wanted and then emit new Wanteds for the antecedents of the Given implication.

I was initially concerned about overlap here -- what if an implication Given's RHS overlaps with a global instance? -- but this was a red herring. Givens have always potentially overlapped with global instances, and very few people are bothered. For example:

min :: Ord a => a -> a -> a

If we call min at type Int, the Ord constraint is potentially ambiguous: do we mean the dictionary supplied or the global Ord Int dictionary? Of course, we mean the local one, and we don't require -XIncoherentInstances to do so. So, worrying about overlap in the context of implication Givens is a red herring. We have a clear rule: local constraints always shadow global ones. That's nice, simple, and unsurprising.

This also doesn't change the "GHC never backtracks" principle. If a local implication-constraint's RHS matches, it is used, just like if GHC finds a global implication constraint (read, global constrained instance).

To implement this, GHC would also need to be able to produce the witness for an implication constraint, but this is just like inferring the lambdas for a higher-rank type. I don't see any challenge here.

Of course, a niggling feeling tells me that this has to be harder than I'm seeing it. But, really, all I see standing in the way is a bit of plumbing.

Thoughts?

comment:15 Changed 3 years ago by simonpj

I agree that much of this is not hard. And it's certainly useful. Indeed it is explicitly discussed in our Haskell Workshop 2000 paper Derivable Type Classes.

The issues I see are:

  • Inference. If users can write such instances, they will probably expect them to be inferred. But that may wrongly defer a type error from a function to its call sites, by inferring an implication which is actually unsatisfiable.
  • Completeness. "Given" constraints interact with each other. How do "given" implications interact with simple "givens"?
  • Impredicativity. Can a constraint variable c be instantiated with one of these implications? Perhaps it's just a question of ruling that out.

comment:16 Changed 3 years ago by goldfire

  • Inference: We don't. Just like we don't infer higher-rank types (which, of course, are the same as implication constraints). If a user wants this feature, they have to ask for it.
  • Completeness: This is thornier. Here is how I see a problem arising:
class C a
class D a
instance D Int

needsD :: D a => a -> ()
implic :: (forall a. C a => D a) -> ()
implic = needsD (5 :: Int)

When typechecking implic, the local universal dictionary for D a will be used to provide a dictionary to needsD. This will then generate an unsatisfiable wanted C Int. But, of course, we could have just used the global instance D Int instead.

An issue such as this one can't arise today (even with local dictionaries shadowing global ones) because local dictionaries never give rise to new wanteds. If you have a local dictionary, it's good to use.

Given/Given interactions would be the same. If one implication-Given can be used in an interaction, it would be, giving rise to its antecedent Wanted constraints.

This does get me a little worried about nondeterminism. But, I conjecture that if this interaction can give rise to nondeterminism, then it would be possible to exhibit the nondeterminism today, using overlapping instances.

So, it all comes down to specifying completeness against what spec, and I'm saying that we could be complete against a spec where every local constraint shadows every overlapped global one. That is, when (forall a. C a => D a) is in scope, instance D Int is not. Will this be easy enough to use to make it practicable? There will be some surprises around it, but I think it's all quite easy to digest with a little guidance. (Certainly easier to understand than closed type families!)

  • Impredicativity: This, to me, is just like the story in kind *. c should be forbidden from unifying with an implication constraint.

comment:17 Changed 3 years ago by simonpj

I'm not against it.

Simon

comment:18 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:19 Changed 3 years ago by thoughtpolice

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:20 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:21 Changed 23 months ago by thomie

Milestone: 8.0.1

comment:22 Changed 18 months ago by goldfire

#12245 is further motivation for solving this.

comment:23 Changed 18 months ago by Iceland_jack

Cc: Iceland_jack added

comment:24 Changed 17 months ago by RyanGlScott

Cc: RyanGlScott added

comment:25 Changed 17 months ago by Iceland_jack

From Proof Relevant Corecursive Resolution, I will copy the relevant text:

Derivable type classes

Hinze and Peyton Jones wanted to use an instance of the form

instance (Binary a, Binary (f (GRose f a))) => Binary (GRose  f a)

but discovered that it causes resolution to diverge. They suggested the following as a replacement:

instance (Binary a, b. Binary b => Binary (f b)) => Binary (GRose f a)

Unfortunately, Haskell does not support instances with polymorphic higher-order instance contexts. Nevertheless, allowing such implication constraints would greatly increase the expressivity of corecursive resolution. In the terminology of our paper, it amounts to extending Horn formulas to intuitionistic formulas. Working with intuitionistic formulas would require a certain amount of searching, as the non-overlapping condition for Horn formulas is not enough to ensure uniqueness of the evidence. For example, consider the following axioms:

κ₁ : (A ⇒ B x) ⇒ D (S x)
ĸ₂ : A, D x ⇒ B (S x)
κ₃ : ⇒ D Z

We have two distinct proof terms for D (S (S (S (S Z)))):

κ₁ (λα₁. ĸ₂ α₁ (ĸ₁ (λα₂. ĸ₂ α₁ ĸ₃))
κ₁ (λα₁. ĸ₂ α₁ (ĸ₁ (λα₂. ĸ₂ α₂ ĸ₃))

This is undesirable from the perspective of generating evidence for type class.


Haskell code

data A
data B a
data D a
data S a
data Z

#393

k1 :: (A -> B x) -> D (S x)
k2 :: A -> D x -> B (S x)
k3 :: D Z

#10843

one, two :: D (S (S (S (S Z))))
one = k1 \a1 -> k2 a1 (k1 \a2 -> k2 a1 k3)
two = k1 \a1 -> k2 a1 (k1 \a2 -> k2 a2 k3)
Last edited 17 months ago by Iceland_jack (previous) (diff)

comment:26 in reply to:  16 Changed 9 months ago by nfrisby

Does the following claim hold water and/or illuminate anything?

The implication constraint on implic can either be simplified (eg C a immediately refines a and/or has D a as a superclass) or it is only satisfiable by a parametric instance of D. Suppose that overlapping and incoherent instances are not allowed. Then any non-parametric instance of D (eg your D Int) would immediately render that implication constraint unsatisfiable.

So the concern is just yet another due solely to overlapping/incoherent instances?

Replying to goldfire:

  • Inference: We don't. Just like we don't infer higher-rank types (which, of course, are the same as implication constraints). If a user wants this feature, they have to ask for it.
  • Completeness: This is thornier. Here is how I see a problem arising:
class C a
class D a
instance D Int

needsD :: D a => a -> ()
implic :: (forall a. C a => D a) -> ()
implic = needsD (5 :: Int)

When typechecking implic, the local universal dictionary for D a will be used to provide a dictionary to needsD. This will then generate an unsatisfiable wanted C Int. But, of course, we could have just used the global instance D Int instead.

An issue such as this one can't arise today (even with local dictionaries shadowing global ones) because local dictionaries never give rise to new wanteds. If you have a local dictionary, it's good to use.

Given/Given interactions would be the same. If one implication-Given can be used in an interaction, it would be, giving rise to its antecedent Wanted constraints.

This does get me a little worried about nondeterminism. But, I conjecture that if this interaction can give rise to nondeterminism, then it would be possible to exhibit the nondeterminism today, using overlapping instances.

So, it all comes down to specifying completeness against what spec, and I'm saying that we could be complete against a spec where every local constraint shadows every overlapped global one. That is, when (forall a. C a => D a) is in scope, instance D Int is not. Will this be easy enough to use to make it practicable? There will be some surprises around it, but I think it's all quite easy to digest with a little guidance. (Certainly easier to understand than closed type families!)

  • Impredicativity: This, to me, is just like the story in kind *. c should be forbidden from unifying with an implication constraint.

comment:27 in reply to:  14 Changed 9 months ago by nfrisby

Your min discussion was helpful to me, but I think it's mostly unrelated, in retrospect; the Ord a dictionary -- again ignoring overlapping/incoherent instances -- could only ever "overlap" with a parametric instance of Ord, since a is skolem. #9701, on the other hand, seems to demonstrate exactly what you were getting at (#12791 too?).

Replying to goldfire:

I initially put this ticket into my internal notes as "Difficulty: Rocket Science", but I've changed my mind. I think this is actually straightforward to implement.

GHC already has implication constraints, except that they're effectively all Wanteds. So, all we would need are to be able to make Given implication constraints. But, these should be rather straightforward, because we can view top-level instances as Given implication constraints. We can just adapt the current look-in-Givens algorithm to do some matching, just like the instance-selection algorithm does. When we find an implication-constraint Given that matches a Wanted, we use it to solve the Wanted and then emit new Wanteds for the antecedents of the Given implication.

I was initially concerned about overlap here -- what if an implication Given's RHS overlaps with a global instance? -- but this was a red herring. Givens have always potentially overlapped with global instances, and very few people are bothered. For example:

min :: Ord a => a -> a -> a

If we call min at type Int, the Ord constraint is potentially ambiguous: do we mean the dictionary supplied or the global Ord Int dictionary? Of course, we mean the local one, and we don't require -XIncoherentInstances to do so. So, worrying about overlap in the context of implication Givens is a red herring. We have a clear rule: local constraints always shadow global ones. That's nice, simple, and unsurprising.

This also doesn't change the "GHC never backtracks" principle. If a local implication-constraint's RHS matches, it is used, just like if GHC finds a global implication constraint (read, global constrained instance).

To implement this, GHC would also need to be able to produce the witness for an implication constraint, but this is just like inferring the lambdas for a higher-rank type. I don't see any challenge here.

Of course, a niggling feeling tells me that this has to be harder than I'm seeing it. But, really, all I see standing in the way is a bit of plumbing.

Thoughts?

Note: See TracTickets for help on using tickets.