Skip to content

type variables appearing only in type equality constraints are not generalized

{-# LANGUAGE TypeFamilies, ScopedTypeVariables#-}

class Foo m where
    type Bar m :: *
    action :: m -> Bar m -> m

right x m = action m (Right x)

right' :: (Either a b ~ Bar m, Foo m) => b -> m -> m
right' x m = action m (Right x)

instance Foo Int where
    type Bar Int = Either Int Int
    action m a = either (*) (+) a m

main = print $ right (1::Int) (3 :: Int)

with the above code i get:

*Main> :type right
                                                                                                                           
right :: (Either Int b ~ Bar m, Foo m) => b -> m -> m

without the main definition i get instead:

*Main> :t right
right :: (Either GHC.Prim.Any b ~ Bar m, Foo m) => b -> m -> m

while i expect the correct type to be the one of right'. It looks related to bug #1813 (closed)

Trac metadata
Trac field Value
Version 6.10.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC sanzhiyan@gmail.com
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information