#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