Skip to content

GitLab

  • Menu
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 4,869
    • Issues 4,869
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • 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 Compiler
  • GHCGHC
  • Issues
  • #9090
Closed
Open
Created May 08, 2014 by Andres Löh@kosmikusReporter

Untouchable higher-kinded type variable in connection with RankNTypes, ConstraintKinds and TypeFamilies

I have the following module

{-# LANGUAGE RankNTypes, ConstraintKinds, TypeFamilies #-}

import GHC.Exts (Constraint)

type family D (c :: Constraint) :: Constraint
type instance D (Eq a) = Eq a

-- checks
f :: Eq b => (forall a. D (Eq a) => f a -> Bool) -> f b -> Bool
f g x = g x

-- checks
f' :: Eq b => (forall a. Eq a => f a -> Bool) -> f b -> Bool
f' = f

-- checks, so GHC seems to think that both types are interchangeable
f'' :: Eq b => (forall a. D (Eq a) => f a -> Bool) -> f b -> Bool
f'' = f'

-- checks
test' y = f' (\ (Just x) -> x /= x) y

-- fails
test y = f (\ (Just x) -> x /= x) y

-- fails too, unsurprisingly
test'' y = f'' (\ (Just x) -> x /= x) y

The module checks with GHC-7.6.3, but fails in GHC-7.8.2 and GHC-7.9.20140430 with

src/Test.hs:24:16:
    Couldn't match type ‘f’ with ‘Maybe’
      ‘f’ is untouchable
        inside the constraints (D (Eq a))
        bound by a type expected by the context: (D (Eq a)) => f a -> Bool
        at src/Test.hs:24:10-35
      ‘f’ is a rigid type variable bound by
          the inferred type of test :: Eq b => f b -> Bool
          at src/Test.hs:24:1
    Possible fix: add a type signature for ‘test’
    Expected type: f a
      Actual type: Maybe a
    Relevant bindings include
      y :: f b (bound at src/Test.hs:24:6)
      test :: f b -> Bool (bound at src/Test.hs:24:1)
    In the pattern: Just x
    In the first argument of ‘f’, namely ‘(\ (Just x) -> x /= x)’
    In the expression: f (\ (Just x) -> x /= x) y

src/Test.hs:27:20:
    Couldn't match type ‘f’ with ‘Maybe’
      ‘f’ is untouchable
        inside the constraints (D (Eq a))
        bound by a type expected by the context: (D (Eq a)) => f a -> Bool
        at src/Test.hs:27:12-39
      ‘f’ is a rigid type variable bound by
          the inferred type of test'' :: Eq b => f b -> Bool
          at src/Test.hs:27:1
    Possible fix: add a type signature for ‘test''’
    Expected type: f a
      Actual type: Maybe a
    Relevant bindings include
      y :: f b (bound at src/Test.hs:27:8)
      test'' :: f b -> Bool (bound at src/Test.hs:27:1)
    In the pattern: Just x
    In the first argument of ‘f''’, namely ‘(\ (Just x) -> x /= x)’
    In the expression: f'' (\ (Just x) -> x /= x) y

I'd expect it to typecheck.

At first, I thought this might be related in some way to #8985 (closed). That's why I tested with HEAD, but while #8985 (closed) seems indeed to be fixed, this is still a problem there.

Also, while my simplified test case compiles with GHC-7.6.3, my original more complicated program does not, so there might be another report forthcoming if I manage to isolate the difference.

Trac metadata
Trac field Value
Version 7.8.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
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