Type equality makes type variable untouchable
This doesn't look right:
{-# LANGUAGE RankNTypes, TypeFamilies #-}
type family TF (m :: * -> *)
run1 :: (forall m . Monad m => m a) -> a
run1 = undefined
run2 :: (forall m . (Monad m, TF m ~ ()) => m a) -> a
run2 = undefined
-- this works
x1 = run1 (return ())
-- this fails
x2 = run2 (return ())
{-
Couldn't match expected type ‘a’ with actual type ‘()’
‘a’ is untouchable
inside the constraints (Monad m, TF m ~ ())
bound by a type expected by the context:
(Monad m, TF m ~ ()) => m a
at untouchable.hs:15:6-21
‘a’ is a rigid type variable bound by
the inferred type of x2 :: a at untouchable.hs:15:1
Relevant bindings include x2 :: a (bound at untouchable.hs:15:1)
In the first argument of ‘return’, namely ‘()’
In the first argument of ‘run2’, namely ‘(return ())’
-}
I would expect x2 to type check just like x1 does.
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 |