Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,242
    • Issues 5,242
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 568
    • Merge requests 568
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #9316
Closed
Open
Issue created Jul 15, 2014 by Ollie Charles@ocharles

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

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking