#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