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
  • #5591
Closed
Open
Issue created Oct 28, 2011 by daniel.is.fischer@trac-daniel.is.fischer

Type constructor variables not injective

I'm not sure whether it is a bug, but there have been two recent reports of ghc-7.2.1 not treating type constructor variables as injective. First, by Daniel Schüssler,

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}
module DTest where

data a :=: b where 
    Refl :: a :=: a

subst :: a :=: b -> f a -> f b
subst Refl = id 

-- Then this doesn't work (error message at the bottom):

inj1 :: forall f a b. f a :=: f b -> a :=: b
inj1 Refl = Refl

-- But one can still construct it with a trick that Oleg used in the context of 
-- Leibniz equality:

type family Arg fa

type instance Arg (f a) = a

newtype Helper fa fa' = Helper { runHelper :: Arg fa :=: Arg fa' }

inj2 :: forall f a b. f a :=: f b -> a :=: b
inj2 p = runHelper (subst p (Helper Refl :: Helper (f a) (f a)))

{-
DTest.hs:13:13:
    Could not deduce (a ~ b)
    from the context (f a ~ f b)
      bound by a pattern with constructor
                 Refl :: forall a. a :=: a,
               in an equation for `inj1'
      at DTest.hs:13:6-9
      `a' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
      `b' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
    Expected type: a :=: b
      Actual type: a :=: a
    In the expression: Refl
    In an equation for `inj1': inj1 Refl = Refl
-}

compiles fine with ghc-7.0.4. Second, by Sjoerd Visscher,

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, 
    GADTs, FlexibleInstances, FlexibleContexts #-}
module STest where

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

{-
STest.hs:12:32:
    Could not deduce (a1 ~ a)
    from the context (Monad m)
      bound by the instance declaration at STest.hs:11:10-59
    or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
      bound by a pattern with constructor
                 CatchError :: forall (m :: * -> *) e a.
                               (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
               in an equation for `fin'
      at STest.hs:12:8-19
      `a1' is a rigid type variable bound by
           a pattern with constructor
             CatchError :: forall (m :: * -> *) e a.
                           (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
           in an equation for `fin'
           at STest.hs:12:8
      `a' is a rigid type variable bound by
          the instance declaration at STest.hs:11:46
    Expected type: e1 -> m a1
      Actual type: e -> m a
    In the first argument of `f', namely `h'
    In the expression: f h
-}

also compiles fine with 7.0.4. ghc-7.3.20111026 behaves like 7.2.1. Which version behaves correctly?

Trac metadata
Trac field Value
Version 7.2.1
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