Opened 2 months ago

#13975 new bug

GHC can't infer pattern signature, untoucable kinds

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

pattern DD :: () => (a ~ D, b ~ D, res ~ '(a, b)) => SPair res
pattern DD <- SPair SD SD

Change History (0)

Note: See TracTickets for help on using tickets.