#11608 closed bug (fixed)

Possible type-checker regression in GHC 8.0 when compiling `microlens`

Reported by: hvr Owned by: simonpj
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc2
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T11608
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I just updated the GHC 8.0 snapshot I was using from 8.0.0.20160214-g977fb8 to 8.0.0.20160218-g23baff7, and suddenly hackage:microlens-0.4.2.0 fails to build with

...
Preprocessing library microlens-0.4.2.0...
[1 of 4] Compiling Lens.Micro.Type  ( src/Lens/Micro/Type.hs, dist/build/Lens/Micro/Type.o )
[2 of 4] Compiling Lens.Micro.Internal ( src/Lens/Micro/Internal.hs, dist/build/Lens/Micro/Internal.o )

src/Lens/Micro/Internal.hs:184:3: error:
    • Couldn't match type ‘s’ with ‘g0 a’
        ‘s’ is untouchable
          inside the constraints: (Traversable g,
                                   s ~ g a,
                                   t ~ g b,
                                   Applicative f)
          bound by the type signature for:
                     each :: (Traversable g, s ~ g a, t ~ g b, Applicative f) =>
                             (a -> f b) -> s -> f t
          at src/Lens/Micro/Internal.hs:184:3-27
    • In the ambiguity check for ‘each’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        each :: forall s t a b. Each s t a b => Traversal s t a b
      In the class declaration for ‘Each’

...is this a regression or a feature? :-)

Change History (19)

comment:1 Changed 20 months ago by hvr

hackage:free-4.12.4 has a similiar sudden failure:

Preprocessing library free-4.12.4...
[ 1 of 16] Compiling Control.Monad.Free.TH ( src/Control/Monad/Free/TH.hs, dist/build/Control/Monad/Free/TH.o )
[ 2 of 16] Compiling Control.Monad.Free.Class ( src/Control/Monad/Free/Class.hs, dist/build/Control/Monad/Free/Class.o )

src/Control/Monad/Free/Class.hs:106:3: error:
    • Couldn't match type ‘m’ with ‘t0 n0’
        ‘m’ is untouchable
          inside the constraints: (m ~ t n,
                                   MonadTrans t,
                                   MonadFree f n,
                                   Functor f)
          bound by the type signature for:
                     wrap :: (m ~ t n, MonadTrans t, MonadFree f n, Functor f) =>
                             f (m a) -> m a
          at src/Control/Monad/Free/Class.hs:106:3-24
    • In the ambiguity check for ‘wrap’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        wrap :: forall (f :: * -> *) (m :: * -> *).
                MonadFree f m =>
                forall a. f (m a) -> m a
      In the class declaration for ‘MonadFree’

comment:2 Changed 20 months ago by RyanGlScott

Specifically, the issue seems to pertain to type equalities in default signatures in typeclasses. Here is the failing code, reduced to reproducible examples:

From microlens:

{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

class Each s t a b | s -> a, t -> b, s b -> t, t a -> s where
  each :: Traversal s t a b
  default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
  each = traverse

From free:

{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

class MonadTrans t where
  lift :: Monad m => m a -> t m a

class Monad m => MonadFree f m | m -> f where
  wrap :: f (m a) -> m a
  default wrap :: (m ~ t n, MonadTrans t, MonadFree f n, Functor f) => f (m a) -> m a
  wrap = join . lift . wrap . fmap return

comment:3 Changed 20 months ago by bgamari

Type of failure: None/UnknownGHC rejects valid program
Version: 8.0.1-rc2

comment:4 Changed 20 months ago by hvr

Just to be clear, afaik this doesn't occur with 8.0.1-rc2, but rather with a more recent 8.0.01 snapshot (as described in the description).

comment:5 Changed 20 months ago by hvr

Cc: goldfire added

It seems like e1631b3b58b7440d3d5a8bf72f1490df635792fb may have been the culprit

comment:6 Changed 20 months ago by hvr

I've temporarily reverted e1631b3b58b7440d3d5a8bf72f1490df635792fb in the ghc-8.0 branch only, via 881b6ccf5c1dbc09d1d16b1b4643e3dec9387047.

I'm not reverting this in GHC HEAD yet, waiting for Richard to comment how we should proceed here.

comment:7 Changed 20 months ago by goldfire

Owner: set to goldfire

I think there's an underlying problem here and that putting the fundep back in is not necessarily the right solution. Will need to look a bit deeper to really know.

comment:8 Changed 20 months ago by simonpj

Aha. In a class decl we use a TyVar (not a skolem TcTyVar) for the class variable(s). (There is a good reason for this: in the final Class value we don't want any TcTyVars.)

Then in TcFlatten.flatten_tyvar we see

flatten_tyvar tv
  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
  = flatten_tyvar3 tv

This case catches that class variable. In the ambiguity check for the type sig for each we have a Given equality for the class variable. Then, because of the above test we fail to take advantage of the Given. (And the error message too is misleading.)

Solution: delete the above equation, so that we treat TyVar and skolem TcTyVar the same. I'm validating now.

The TyVar/TcTyVar story is not great.

comment:9 Changed 20 months ago by simonpj

Owner: changed from goldfire to simonpj

Actually there's a better way. Anyway I'm on this.

Simon

comment:10 Changed 20 months ago by Simon Peyton Jones <simonpj@…>

In 7496be5c/ghc:

Exclude TyVars from the constraint solver

There is a general invariant that the constraint solver doesn't see
TyVars, only TcTyVars.  But when checking the generic-default
signature of a class, we called checkValidType on the generic-default
type, which had the class TyVar free. That in turn meant that it wasn't
considered during flattening, which led to the error reported in
Trac #11608.

The fix is simple: call checkValidType on the /closed/ type. Easy.

While I was at it, I added a bunch of ASSERTs about the TcTyVar
invariant.

comment:11 Changed 20 months ago by simonpj

NB: the isTcTyVar could conceivably cause extra ASSERT failures when DEBUG is on. I didn't see any, but keep your eyes open.

However, ignoring them (ie no -DDEBUG) is simply what happens today and is fine. So things will not be worse.

Simon

comment:12 Changed 20 months ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T11608

comment:13 Changed 20 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:14 Changed 20 months ago by goldfire

Hm. These ASSERTs used to be here, and I removed them because they were triggering on kind variables, which were not always TcTyVars. However, if the dependent set of tests in the testsuite aren't failing here, then perhaps things improved from when I removed the ASSERTs.

comment:15 Changed 20 months ago by simonpj

It seems that way, but I did not do a full stage2 build with DEBUG on. Thomie may do that for us :-)

comment:16 Changed 20 months ago by thomie

Travis is reporting this at the moment:

Unexpected failures:
   polykinds                 MonoidsTF [exit code non-0] (normal)
   polykinds                 T11480b [exit code non-0] (normal)
   polykinds                 T11523 [exit code non-0] (normal)
   th                        T3100 [exit code non-0] (normal)
   typecheck/should_compile  T3692 [exit code non-0] (normal)
   typecheck/should_fail     T3592 [stderr mismatch] (normal)
   typecheck/should_fail     TcCoercibleFail [stderr mismatch] (normal)
Last edited 20 months ago by thomie (previous) (diff)

comment:17 Changed 20 months ago by simonpj

Jolly good.

  • The polykinds ones are discussed in #11648
  • TcCoercibleFail is really supposed to fail with -DDEBUG (exponential sized types)
  • I have a patch coming for the other three.

So this is good news really.

comment:18 Changed 20 months ago by simonpj

Status: closedmerge

Here's the patch for the other three

commit 3c29c770be7a8c7268dcb8d8624853428aa42071
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Feb 29 14:12:28 2016 +0000

    Do not check synonym RHS for ambiguity
    
    With this patch we no longer check the RHS of a type synonym
    declaration for ambiguity.  It only affects type synonyms with foralls
    on the RHS (which are rare in the first place), and it's arguably
    over-aggressive to check them for ambiguity.  See TcValidity
    Note [When we don't check for ambiguity]
    
    This fixes the ASSERT failures in
       th                        T3100
       typecheck/should_compile  T3692
       typecheck/should_fail     T3592

Just about worth merging.

comment:19 Changed 20 months ago by bgamari

Status: mergeclosed

comment:18 has been merged to ghc-8.0 as 43163e3bd5bcd7c92fc692b365be750a7b766026.

Note: See TracTickets for help on using tickets.