[GHC] #13537: Adding underscore (m :: _) to pattern variable makes it fail

6 Apr 2017

      #13537: Adding underscore (m :: _) to pattern variable makes it fail
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This works fine

 {{{#!hs
 {-# 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

 {{{#!hs
 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>
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler