GitLab

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!

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture