Unexpected error about untouchable variable
Hello! I've got a strange error here. Let's consider the following code:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
data X
data Expr a = Expr Int
type family Sum a b
type instance Sum X X = X
app :: Expr l -> (Expr l') -> m (Expr (Sum l l'))
app = undefined
finish :: Builder (Expr l) -> Builder (Expr X)
finish = undefined
type family Foo (m :: * -> *) :: * -> *
class (Monad m, Foo (Foo m) ~ Foo m) => Ctx (m :: * -> *)
newtype Builder a = Builder (forall m. Ctx m => m a)
f :: Builder (Expr X) -> Builder (Expr X) -> Builder (Expr X) -> Builder (Expr X)
f mop ma mb = finish $ Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X))
main :: IO ()
main = return ()
it results in error:
UT.hs:24:34: error:
• Couldn't match type ‘l0’ with ‘X’
‘l0’ is untouchable
inside the constraints: Ctx m
bound by a type expected by the context:
Ctx m => m (Expr l0)
at UT.hs:24:24-84
Expected type: m (Expr l0)
Actual type: m (Expr (Sum X X))
• In the second argument of ‘($)’, namely
‘app (undefined :: Expr X) (undefined :: Expr X)’
In the second argument of ‘($)’, namely
‘Builder $ app (undefined :: Expr X) (undefined :: Expr X)’
In the expression:
finish $ Builder $ app (undefined :: Expr X) (undefined :: Expr X)
And that's very interesting, because it should (according to my knowledge) not happen. It is caused by the line: finish $ Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X))
.
And we can observe here couple of things. First of all app :: Expr l -> (Expr l') -> m (Expr (Sum l l'))
and Sum X X = X
, so app (undefined :: (Expr X)) (undefined :: (Expr X)) :: Expr X
- and GHC can clearly see it.
What is more interesting is that if we put this signature explicitly it works! So If we change the error line to:
...
f mop ma mb = finish $ (Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X)) :: Builder (Expr X)
it compiles fine.
Another interesting fact is that if I remove the constraint Foo (Foo m) ~ Foo m
it also compiles fine, which is even more strange.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |