[GHC] #13975: GHC can't infer pattern signature, untoucable kinds

14 Jul 2017

      #13975: GHC can't infer pattern signature, untoucable kinds
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.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:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language TypeFamilyDependencies, TypeInType, KindSignatures,
 PolyKinds, PatternSynonyms, GADTs #-}

 import Data.Kind

 data T = D | I

 type SING k = k -> Type

 type family
   Sing = (r :: SING k) | r -> k where
   Sing = ST
   Sing = SPair

 data ST :: SING T where
   SD :: ST D
   SI :: ST I

 data SPair :: SING (k, k') where
   SPair :: Sing a -> Sing b -> SPair '(a, b)

 pattern DD :: SPair '(D, D)
 pattern DD = SPair SD SD
 }}}

 works.. until we remove the pattern signature for `DD`, then we get

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

 /tmp/aur.hs:21:20: error:
     • Couldn't match kind ‘k’ with ‘T’
         ‘k’ is untouchable
           inside the constraints: t ~ '(a, b)
           bound by a pattern with constructor:
                      SPair :: forall k k' (a :: k) (b :: k').
                               Sing a -> Sing b -> SPair '(a, b),
                    in a pattern synonym declaration
           at /tmp/aur.hs:21:14-24
       ‘k’ is a rigid type variable bound by
         the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
       Possible fix: add a type signature for ‘DD’
       When matching the kind of ‘a’
       Expected type: Sing a
         Actual type: ST a
     • In the pattern: SD
       In the pattern: SPair SD SD
       In the declaration for pattern synonym ‘DD’

 /tmp/aur.hs:21:23: error:
     • Couldn't match kind ‘k'’ with ‘T’
         ‘k'’ is untouchable
           inside the constraints: a ~ 'D
           bound by a pattern with constructor: SD :: ST 'D,
                    in a pattern synonym declaration
           at /tmp/aur.hs:21:20-21
       ‘k'’ is a rigid type variable bound by
         the inferred type of DD :: SPair t at /tmp/aur.hs:21:9
       Possible fix: add a type signature for ‘DD’
       When matching the kind of ‘b’
       Expected type: Sing b
         Actual type: ST b
     • In the pattern: SD
       In the pattern: SPair SD SD
       In the declaration for pattern synonym ‘DD’
 Failed, modules loaded: none.
 }}}

 Restricting the kind of `SPair` to `SPair :: SING (T, T)` gets it to work,
 can it be made to work bidirectionally? Or can it only work
 unidirectionally

 {{{#!hs
 pattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res
 pattern DD <- SPair SD SD
 }}}

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