[GHC] #9316: GHC 7.8.3 no longer infers correct type in presence of type families and constraints

15 Jul 2014

      #9316: GHC 7.8.3 no longer infers correct type in presence of type families and
constraints
-------------------------------------+-------------------------------------
        Reporter:  ocharles          |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.8.3
        Keywords:                    |  Differential Revisions:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
       Test Case:                    |              Difficulty:  Unknown
        Blocking:                    |              Blocked By:
                                     |         Related Tickets:
-------------------------------------+-------------------------------------
 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!

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9316
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler