Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#14363 closed bug (fixed)

:type hangs on coerce

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: Roles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T14363, T14363a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

This works

$ ghci -ignore-dot-ghci
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> import Data.Coerce
Prelude Data.Coerce> :t [fmap, coerce]

<interactive>:1:8: error:
    • Occurs check: cannot construct the infinite type: b ~ f b
        arising from a use of ‘coerce’
    • In the expression: coerce
      In the expression: [fmap, coerce]

But doing it with contra

Prelude Data.Coerce> contra = undefined :: Functor f => (b -> a) -> (f a -> f b)

it hangs

Prelude Data.Coerce> :t [coerce, contra]
^CInterrupted.
Prelude Data.Coerce> :t [contra, coerce]
^CInterrupted.

Change History (9)

comment:1 Changed 2 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 2 years ago by Iceland_jack

Functor constraint not needed to make it hang

Prelude Data.Coerce> contra = undefined :: (a -> b) -> (f b -> f a)
Prelude Data.Coerce> :t [contra, coerce]
^CInterrupted.

Giving it a concrete type gives an actual failure

Prelude Data.Coerce> contra = undefined :: (a -> b) -> (Maybe b -> Maybe a)
Prelude Data.Coerce> :t [contra, coerce]

<interactive>:1:10: error:
    • Occurs check: cannot construct the infinite type:
        b ~ Maybe (Maybe b)
        arising from a use of ‘coerce’
    • In the expression: coerce
      In the expression: [contra, coerce]

comment:3 Changed 2 years ago by simonpj

Gah! How has this bug survived so long? I see this

Inert set:   [G] co1:  a  ~R#  f b
Work item:   [G] co2:  b  ~R#  f a

We can't rewrite the work item co2 with the inert co1, because the role of f's argument is Nominal, sotco1 can't rewrite it.

So we add co2 to the inert set. Alas we then kick out co1 becuase it has a free b, thinking that it might be rewritten by co2. But of course it can't and we get an infinite loop instead. Sigh!

What's wrong? I think that anyRewritableTyVar needs to beecome role-aware.

Richard do you agree?

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

comment:4 Changed 2 years ago by Iceland_jack

Keywords: Roles added

comment:5 Changed 2 years ago by goldfire

Yes, anyRewritableTyVar needs to become role-aware. It should pass a role to the predicate function, I think.

But I'm not sure why the "occurs check" failure in the original post is correct. IIUC, we're trying to check coerce :: (a -> b) -> (f a -> f b). In other words, we want to prove Coercible (a -> b) (f a -> f b), which decomposes to Coercible a (f a) and Coercible b (f b). These aren't insoluble, and I don't think we should report an occurs-check problem.

comment:6 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 3acd616/ghc:

Improve kick-out in the constraint solver

This patch was provoked by Trac #14363.  Turned out that we were
kicking out too many constraints in TcSMonad.kickOutRewritable, and
that mean that the work-list never became empty: infinite loop!

That in turn made me look harder at the Main Theorem in
Note [Extending the inert equalities].

Main changes

* Replace TcType.isTyVarExposed by TcType.isTyVarHead.  The
  over-agressive isTyVarExposed is what caused Trac #14363.
  See Note [K3: completeness of solving] in TcSMonad.

* TcType.Make anyRewriteableTyVar role-aware.  In particular,
      a ~R ty
  cannot rewrite
      b ~R f a
  See Note [anyRewriteableTyVar must be role-aware].  That means
  it has to be given a role argument, which forces a little
  refactoring.

  I think this change is fixing a bug that hasn't yet been reported.
  The actual reported bug is handled by the previous bullet.  But
  this change is definitely the Right Thing

The main changes are in TcSMonad.kick_out_rewritable, and in TcType
(isTyVarExposed ---> isTyVarHead).

I did a little unforced refactoring:

 * Use the cc_eq_rel field of a CTyEqCan when it is available, rather
   than recomputing it.

 * Define eqCanRewrite :: EqRel -> EqRel -> EqRel, and use it, instead
   of duplicating its logic

comment:7 Changed 2 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14363, T14363a

My patch fixes the loop. The occurs-check problem was already fixed, perhaps by my wc_insol changes. I've added tests for both.

Richard I'd appreciate a quick look at the patch, but I'm pretty confident (following our discussion) hence committing. Perhaps you can then close.

comment:8 Changed 2 years ago by Iceland_jack

Thank you Simon. A coworker of mine met you at yesterday's Papers We Love, she said you were working on a patch fixing a loop in the type checker :] I'm curious if this was it

comment:9 Changed 2 years ago by simonpj

Yes, that was it :-).

Note: See TracTickets for help on using tickets.