[GHC] #15685: Pattern signature not inferred

[GHC]

#15685: Pattern signature not inferred
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Should this pattern synonym declaration fail,

 {{{#!hs
 {-# Language DataKinds, TypeOperators, PolyKinds, GADTs, PatternSynonyms
 #-}

 import Data.Kind

 data NS f as where
  Here :: f a -> NS f (a:as)

 data NP :: (k -> Type) -> ([k] -> Type) where
  Nil :: NP f '[]

 pattern HereNil = Here Nil
 }}}

 {{{
 $ ghci -ignore-dot-ghci hs/457.hs
 GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( hs/457.hs, interpreted ) [flags
 changed]

 hs/457.hs:11:19: error:
     • Could not deduce: f ~~ NP f0
       from the context: (as ~ (a1 : as1), GHC.Types.Any ~ '[])
         bound by the signature for pattern synonym ‘HereNil’
         at hs/457.hs:11:1-26
       ‘f’ is a rigid type variable bound by
         the signature for pattern synonym ‘HereNil’
         at hs/457.hs:11:1-26
       Expected type: NS f as
         Actual type: NS (NP f0) ('[] : as0)
     • In the expression: Here Nil
       In an equation for ‘HereNil’: HereNil = Here Nil
     • Relevant bindings include
         $bHereNil :: NS f as (bound at hs/457.hs:11:9)
    |
 11 | pattern HereNil = Here Nil
    |                   ^^^^^^^^

 hs/457.hs:11:24: error:
     • Kind mismatch: cannot unify (f :: a -> *) with:
         NP a0 :: [GHC.Types.Any] -> *
       Their kinds differ.
       Expected type: f a1
         Actual type: NP a0 GHC.Types.Any
     • In the pattern: Nil
       In the pattern: Here Nil
       In the declaration for pattern synonym ‘HereNil’
    |
 11 | pattern HereNil = Here Nil
    |                        ^^^
 Failed, no modules loaded.
 Prelude>
 }}}

 It can be given a pattern signature, my question is can this not be
 inferred

 {{{#!hs
 -- pattern HereNil :: NS (NP f) ('[]:as)
 pattern HereNil :: () => (nil_as ~ ('[]:as)) => NS (NP f) nil_as
 pattern HereNil = Here Nil
 }}}

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