Adding underscore (m :: _) to pattern variable makes it fail
This works fine
{-# Language RankNTypes, TypeOperators, KindSignatures, GADTs, ScopedTypeVariables, PolyKinds #-}
import Data.Kind
data CodTy :: (k -> Type) -> Type where
CodTy :: { runCodTy :: (forall r. (f ty -> r) -> r) } -> CodTy f
type f ~> g = forall xx. f xx -> g xx
fmap' :: (f ~> f') -> (CodTy f -> CodTy f')
fmap' f (CodTy m) = CodTy $ \ c -> m (c . f)
but adding
fmap' f (CodTy (m :: _)) = CodTy $ \ c -> m (c . f)
makes it fail (also fails without PolyKinds
)
$ ghci -ignore-dot-ghci tNT2.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( tNT2.hs, interpreted )
tNT2.hs:11:22: error:
• Found type wildcard ‘_’ standing for ‘(f ty -> r0) -> r0’
Where: ‘r0’ is an ambiguous type variable
‘f’ is a rigid type variable bound by
the type signature for:
fmap' :: forall k (f :: k -> *) (f' :: k -> *).
f ~> f' -> CodTy f -> CodTy f'
at tNT2.hs:10:10
‘ty’ is a rigid type variable bound by
a pattern with constructor:
CodTy :: forall k (f :: k -> *) (ty :: k).
(forall r. (f ty -> r) -> r) -> CodTy f,
in an equation for ‘fmap'’
at tNT2.hs:11:10
‘k’ is a rigid type variable bound by
the type signature for:
fmap' :: forall k (f :: k -> *) (f' :: k -> *).
f ~> f' -> CodTy f -> CodTy f'
at tNT2.hs:10:10
To use the inferred type, enable PartialTypeSignatures
• In a pattern type signature: _
In the pattern: m :: _
In the pattern: CodTy (m :: _)
• Relevant bindings include
f :: f ~> f' (bound at tNT2.hs:11:7)
fmap' :: f ~> f' -> CodTy f -> CodTy f' (bound at tNT2.hs:11:1)
tNT2.hs:11:46: error:
• Couldn't match type ‘r0’ with ‘r’
because type variable ‘r’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
(f' ty -> r) -> r
at tNT2.hs:11:28-51
Expected type: f ty -> r0
Actual type: f ty -> r
• In the first argument of ‘m’, namely ‘(c . f)’
In the expression: m (c . f)
In the second argument of ‘($)’, namely ‘\ c -> m (c . f)’
• Relevant bindings include
c :: f' ty -> r (bound at tNT2.hs:11:38)
m :: (f ty -> r0) -> r0 (bound at tNT2.hs:11:17)
Failed, modules loaded: none.
Prelude>
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |