GHC can't infer pattern signature, untoucable kinds
{-# 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
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |