Ticket #5595 (closed bug: fixed)

Opened 19 months ago

Last modified 18 months ago

Unification under a forall doesn't allow full constraint solving

Reported by: basvandijk Owned by: simonpj
Priority: normal Milestone: 7.6.1
Component: Compiler Version: 7.2.1
Keywords: Cc: dimitris@…, nathanhowell@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: typecheck/should_compile/T5595 Blocked By:
Blocking: Related Tickets:

Description

As  mentioned on the glasgow-haskell-users mailinglist, I'm working on a new design of  monad-control. However I get a type error I don't understand. Here's an isolated example: 

{-# LANGUAGE UnicodeSyntax, RankNTypes, TypeFamilies #-}

class MonadTransControl t where
  type St t ∷ * → *

  liftControl ∷ Monad m ⇒ (Run t → m α) → t m α

  restore ∷ Monad o ⇒ St t γ → t o γ

type Run t = ∀ n β. Monad n ⇒ t n β → n (St t β)

foo :: (Monad m, MonadTransControl t) => (Run t -> m α) -> t m α
foo f = liftControl f

Type checking foo this gives the following error: 

   Couldn't match expected type `Run t' with actual type `Run t'
   Expected type: Run t -> m α
     Actual type: Run t -> m α
   In the first argument of `liftControl', namely `f'
   In the expression: liftControl f

When I remove the type annotation of foo the program type checks. But when I ask ghci the type of foo it tells me it's the same type: 

> :t foo
foo :: (Monad m, MonadTransControl t) => (Run t -> m α) -> t m α

Note that when I change the associated type synonym to a associated data type the error disappears.

Is this a bug in GHC?

I'm using ghc-7.2.1.

Change History

  Changed 19 months ago by simonpj

  • cc dimitris@… added

follow-up: ↓ 3   Changed 19 months ago by simonpj

Thank you for reporting this. In TcUnify there is this comment: 

          -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
          -- VERY UNSATISFACTORY; the constraint might be fine, but
	  -- we fail eagerly because we don't have any place to put 
	  -- the bindings from an implication constraint
	  -- This only works because most constraints get solved on the fly
	  -- See Note [Avoid deferring]

You are the first to trip over this place, where we took a short cut in the implementation. It's really a bug -- admittedly to do with matching polymorphic types -- and we think we know how to fix it. It it's not just a quick fix (else we'd have done it before now).

The problem is the type function under a higher-rank forall. I don't know a good workaround. We'll get to it, but not instantly. Is it ruining your life?

Simon

in reply to: ↑ 2 ; follow-up: ↓ 4   Changed 19 months ago by basvandijk

Replying to simonpj:

Is it ruining your life?

No, I switched to associated data types which don't have the problem.

Thanks,

Bas

in reply to: ↑ 3   Changed 19 months ago by basvandijk

Replying to basvandijk:

Replying to simonpj:

Is it ruining your life?

No, I switched to associated data types which don't have the problem.

Although this is not ruining my life, I do like to mention that if I could use associated type synonyms I can greatly simply (and hopefully optimize) the  new design of monad-control.

For example, now I have: 

instance MonadTransControl (StateT s) where
    newtype St (StateT s) α = StState (α, s)
    liftControl f = StateT $ \s →
                      liftM (\x → (x, s))
                            (f $ \t → liftM StState $ runStateT t s)
    restoreT (StState st) = StateT $ \_ → return st

It would be nice if this could be simplified to just: 

instance MonadTransControl (StateT s) where
    type St (StateT s) α = (α, s)
    liftControl f = StateT $ \s →
                      liftM (\x → (x, s))
                            (f $ \t → runStateT t s)
    restoreT st = StateT $ \_ → return st

Look: no ugly StState wrappers and no potentially inefficient: liftM StState.

Or take MonadControlIO for example: 

instance MonadControlIO IO where
    newtype StIO IO α = StIO α
    liftControlIO f = f $ liftM StIO
    restore (StIO x) = return x

instance MonadControlIO m ⇒ MonadControlIO (StateT s m) where
    newtype StIO (StateT s m) α = StIOState (ComposeSt (StateT s) m α)
    liftControlIO = liftControlIODefault StIOState
    restore (StIOState stIO) = StateT $ \s → do
                                 st ← restore stIO
                                 runStateT (restoreT st) s

type ComposeSt t m α = StIO m (St t α)

liftControlIODefault ∷ (MonadTransControl t, MonadControlIO m, Monad (t m), Monad m)
                     ⇒ (∀ β. ComposeSt t m β → StIO (t m) β) -- ^ 'StIO' constructor
                     → ((RunInIO (t m) → IO α) → t m α)
liftControlIODefault stIO = \f → liftControl $ \run →
                                   liftControlIO $ \runInIO →
                                     f $ liftM stIO ∘ runInIO ∘ run

This can be neatly simplified to just: 

instance MonadControlIO IO where
    type StIO IO α = α
    liftControlIO f = f id
    restore = return

instance MonadControlIO m ⇒ MonadControlIO (StateT s m) where
    type StIO (StateT s m) α = ComposeSt (StateT s) m α
    liftControlIO = liftControlIODefault
    restore stIO = StateT $ \s → do
                     st ← restore stIO
                     runStateT (restoreT st) s

type ComposeSt t m α = StIO m (St t α)

liftControlIODefault ∷ (MonadTransControl t, MonadControlIO m, Monad (t m), Monad m)
                     → (RunInIO (t m) → IO α) → t m α
liftControlIODefault f = liftControl $ \run →
                           liftControlIO $ \runInIO →
                             f $ runInIO ∘ run

  Changed 18 months ago by simonpj

  • summary changed from Type error: expected type = actual type ??? to Unification under a forall doesn't allow full constraint solving

  Changed 18 months ago by simonpj

See also #4310

  Changed 18 months ago by igloo

  • owner set to simonpj
  • milestone set to 7.6.1

  Changed 18 months ago by nathanhowell

  • cc nathanhowell@… added

  Changed 18 months ago by simonpj@…

commit 2e6dcdf711ebd50eef230a878014a5a9abd20e07 

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Dec 5 04:44:13 2011 +0000

    Allow full constraint solving under a for-all (Trac #5595)
    
    The main idea is that when we unify
        forall a. t1  ~  forall a. t2
    we get constraints from unifying t1~t2 that mention a.
    We are producing a coercion witnessing the equivalence of
    the for-alls, and inside *that* coercion we need bindings
    for the solved constraints arising from t1~t2.
    
    We didn't have way to do this before.  The big change is
    that here's a new type TcEvidence.TcCoercion, which is
    much like Coercion.Coercion except that there's a slot
    for TcEvBinds in it.
    
    This has a wave of follow-on changes. Not deep but broad.
    
    * New module TcEvidence, which now contains the HsWrapper
      TcEvBinds, EvTerm etc types that used to be in HsBinds
    
    * The typechecker works exclusively in terms of TcCoercion.
    
    * The desugarer converts TcCoercion to Coercion
    
    * The main payload is in TcUnify.unifySigmaTy. This is the
      function that had a gross hack before, but is now beautiful.
    
    * LCoercion is gone!  Hooray.
    
    Many many fiddly changes in conssequence.  But it's nice.

 compiler/deSugar/Desugar.lhs          |    2 +-
 compiler/deSugar/DsArrows.lhs         |    1 +
 compiler/deSugar/DsBinds.lhs          |  273 ++++++++--------
 compiler/deSugar/DsExpr.lhs           |   37 +--
 compiler/deSugar/DsListComp.lhs       |    1 +
 compiler/deSugar/Match.lhs            |   20 +-
 compiler/deSugar/MatchCon.lhs         |   13 +-
 compiler/ghc.cabal.in                 |    1 +
 compiler/hsSyn/HsBinds.lhs            |  227 +-------------
 compiler/hsSyn/HsExpr.lhs             |    1 +
 compiler/hsSyn/HsPat.lhs              |    1 +
 compiler/hsSyn/HsUtils.lhs            |   66 ++--
 compiler/main/GHC.hs                  |    2 +-
 compiler/main/GhcMake.hs              |    2 +-
 compiler/parser/Parser.y.pp           |    1 +
 compiler/parser/RdrHsSyn.lhs          |    1 +
 compiler/rename/RnBinds.lhs           |    1 +
 compiler/typecheck/Inst.lhs           |    3 +-
 compiler/typecheck/TcArrows.lhs       |    6 +-
 compiler/typecheck/TcBinds.lhs        |    1 +
 compiler/typecheck/TcCanonical.lhs    |  123 ++++----
 compiler/typecheck/TcClassDcl.lhs     |    1 +
 compiler/typecheck/TcDeriv.lhs        |   12 +-
 compiler/typecheck/TcEnv.lhs          |    8 +-
 compiler/typecheck/TcEvidence.lhs     |  570 +++++++++++++++++++++++++++++++++
 compiler/typecheck/TcExpr.lhs         |   12 +-
 compiler/typecheck/TcForeign.lhs      |    2 +-
 compiler/typecheck/TcHsSyn.lhs        |   53 ++--
 compiler/typecheck/TcHsType.lhs       |    1 +
 compiler/typecheck/TcInstDcls.lhs     |   14 +-
 compiler/typecheck/TcInteract.lhs     |   55 ++--
 compiler/typecheck/TcMatches.lhs      |    6 +-
 compiler/typecheck/TcMatches.lhs-boot |    3 +-
 compiler/typecheck/TcPat.lhs          |   22 +-
 compiler/typecheck/TcRnDriver.lhs     |    3 +-
 compiler/typecheck/TcRnMonad.lhs      |    7 +-
 compiler/typecheck/TcRnTypes.lhs      |    5 +
 compiler/typecheck/TcSMonad.lhs       |   82 ++---
 compiler/typecheck/TcSimplify.lhs     |    5 +-
 compiler/typecheck/TcSplice.lhs       |    1 +
 compiler/typecheck/TcType.lhs         |   10 +-
 compiler/typecheck/TcUnify.lhs        |   79 ++---
 compiler/typecheck/TcUnify.lhs-boot   |    4 +-
 compiler/types/Coercion.lhs           |   98 ++-----
 compiler/types/Type.lhs               |    9 +-
 compiler/types/TypeRep.lhs            |    2 +-
 46 files changed, 1079 insertions(+), 768 deletions(-)

  Changed 18 months ago by basvandijk

Thanks Simon!

This  works beautifully in monad-control.

Will this be in GHC-7.4?

  Changed 18 months ago by simonpj

  • status changed from new to merge
  • difficulty set to Unknown
  • testcase set to typecheck/should_compile/T5595

Test added. Yes this bug fix should be in 7.4.

Setting to 'merge' in case Ian hasn't merged it yet.

Simon

  Changed 18 months ago by igloo

  • status changed from merge to closed
  • resolution set to fixed

Patch is included in 7.4 branch.

Note: See TracTickets for help on using tickets.