Opened 3 years ago

Closed 2 years ago

#9316 closed bug (fixed)

GHC 7.8.3 no longer infers correct type in presence of type families and constraints

Reported by: ocharles Owned by:
Priority: normal Milestone: 7.8.4
Component: Compiler Version: 7.8.3
Keywords: Cc:
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

The following code fails to compile under GHC 7.8.3:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module SingletonsBug where

import Control.Applicative
import Data.Constraint (Dict(..))
import Data.Singletons
import Data.Singletons.TH (singletons)
import Data.Traversable (for)

$(singletons [d|

    data SubscriptionChannel = BookingsChannel

  |])

type family T (c :: SubscriptionChannel) :: *
type instance T 'BookingsChannel = Bool

witnessC :: SSubscriptionChannel channel -> Dict (Show (T channel), SingI channel)
witnessC SBookingsChannel = Dict

forAllSubscriptionChannels
  :: forall m r. (Applicative m)
  => (forall channel. (SingI channel, Show (T channel)) => SSubscriptionChannel channel -> m r)
  -> m r
forAllSubscriptionChannels f =
  withSomeSing BookingsChannel $ \(sChannel) ->
    case witnessC sChannel of
      Dict -> f sChannel
SingletonsBug.hs:38:15:
    Could not deduce (SingI channel0) arising from a use of ‘f’
    from the context (Applicative m)
      bound by the type signature for
                 forAllSubscriptionChannels :: Applicative m =>
                                               (forall (channel :: SubscriptionChannel).
                                                (SingI channel, Show (T channel)) =>
                                                SSubscriptionChannel channel -> m r)
                                               -> m r
      at SingletonsBug.hs:(32,6)-(34,8)
    or from ((Show (T a), SingI a))
      bound by a pattern with constructor
                 Dict :: forall (a :: Constraint). (a) => Dict a,
               in a case alternative
      at SingletonsBug.hs:38:7-10
    The type variable ‘channel0’ is ambiguous
    Note: there is a potential instance available:
      instance SingI 'BookingsChannel -- Defined at SingletonsBug.hs:19:3
    In the expression: f sChannel
    In a case alternative: Dict -> f sChannel
    In the expression: case witnessC sChannel of { Dict -> f sChannel }

SingletonsBug.hs:38:17:
    Couldn't match type ‘channel0’ with ‘a’
      because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: Sing a -> m r
      at SingletonsBug.hs:(36,3)-(38,24)
    Expected type: SSubscriptionChannel channel0
      Actual type: Sing a
    Relevant bindings include
      sChannel :: Sing a (bound at SingletonsBug.hs:36:36)
    In the first argument of ‘f’, namely ‘sChannel’
    In the expression: f sChannel

However, this works fine in GHC 7.8.2.

If I change one line to this:

  withSomeSing BookingsChannel $ \(sChannel :: SSubscriptionChannel c) ->

The code compiles in GHC 7.8.3.

Another change that doesn't require a type signature (but changes the program) is to change that constraint from:

Show (T channel), SingI channel

to just

SingI channel

It seems that the use of the type family breaks the inference, but this might be a bit of a red herring!

Change History (5)

comment:1 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 4b3df0bb705c9287046c07bbc6c038960fbf8d53/ghc:

Further improvements to floating equalities

This equality-floating stuff is horribly delicate!  Trac #9316 showed
up yet another corner case.

The main changes are
 * include CTyVarEqs when "growing" the skolem set
 * do not include the kind argument to (~) when growing the skolem set

I added a lot more comments as well

comment:2 Changed 3 years ago by simonpj

Milestone: 7.8.4
Status: newmerge

I'm not honestly sure exactly what changed between 7.8.2 and 7.8.3, but the fixed code is much more robust. Thank you for this test case. I hope you can work around it for now.

If we ever release 7.8.4 this should go in, so I'll make it patch status on that.

Simon

comment:3 Changed 3 years ago by thoughtpolice

Milestone: 7.8.47.10.1

Moving (in bulk) to 7.10.4

comment:4 Changed 2 years ago by thoughtpolice

Milestone: 7.10.17.8.4

comment:5 Changed 2 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to 7.8.4.

Note: See TracTickets for help on using tickets.