Something is amiss with quantification in pattern synonym type signatures
Consider this program,
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}
module Test where
data AType (a :: k) where
AMaybe :: AType Maybe
AInt :: AType Int
AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). AType a -> AType b -> AType (a b)
pattern PApp :: () => (fun ~ a b) => AType a -> AType b -> AType fun
--pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1).
-- () => (fun ~ a b) => AType a -> AType b -> AType fun
pattern PApp fun arg <- AApp fun arg
I would have thought that the two type signatures would be equivalent. However, when I use the quantified signature GHC complains with,
hi.hs:14:34: error:
• Expected kind ‘AType a’, but ‘fun’ has kind ‘AType a1’
• In the declaration for pattern synonym ‘PApp’
• Relevant bindings include
arg :: AType b1 (bound at hi.hs:14:34)
fun :: AType a1 (bound at hi.hs:14:30)
Moreover, if I use the un-quantified signature and ask GHCi for the full type signature, it gives me the precisely the quantified type that it rejected previously,
λ> :info PApp
pattern PApp :: forall k (fun :: k) k1 (a :: k1
-> k) (b :: k1). () => fun ~ a b => AType a
-> AType b
-> AType fun
-- Defined at hi.hs:14:1
Very odd.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1-rc1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | mpickering |
Operating system | |
Architecture |