#12905: Core lint with pattern synonym
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 8.2.1
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords: typeable
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Description changed by bgamari:
@@ -64,3 +64,3 @@
- It appears that this is yet another case of the kind of `(->)` being too
- restrictive (#11714) since `a -> b` appears to be lifted to the coercion
- `TyConAppCo role (->) [a, b]`.
+ This may be yet another case of the kind of `(->)` being too restrictive
+ (#11714) since `a -> b` appears to be lifted to the coercion `TyConAppCo
+ role (->) [a, b]`.
New description:
Yet another program from the type-indexed `Typeable` effort which breaks
GHC (`master` branch as of 3bd1dd4d75fde3b922d4de08c16f29bdeb8e05d7) with
a core lint error,
{{{#!hs
{-# LANGUAGE GADTs, TypeOperators, PatternSynonyms, TypeInType, PolyKinds,
RankNTypes #-}
module T where
import GHC.Exts
import Data.Kind
import Data.Type.Equality
data TypeRep (a :: k) where
TrTyCon :: TypeRep (a :: k)
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1)
(b :: TYPE r2).
TypeRep a
-> TypeRep b
-> TypeRep (a -> b)
pattern TRFun :: forall k (fun :: k). ()
=> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE
r1) (res :: TYPE r2). (k ~ Type, fun ~~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TrFun arg res
where TRFun arg res = TrFun arg res
}}}
This program produces many core lint errors, although all of them fall
into only a few classes. Here's one,
{{{
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the coercion ‘Sym (Sym cobox_a3fT |> Sym cobox_a3fU)’
Kind application error in
type ‘((->) |> <*>_N ->_N <*>_N ->_N Sym cobox) a’
Function kind = * -> * -> k
Arg kinds = [(a, TYPE r1)]
}}}
{{{
<no location info>: warning:
[RHS of $d~~_a3fO :: (fun :: k) ~~ ((a -> b) :: *)]
Kind application error in
coercion ‘Sym
(Sym
(<(->)>_N |> ((<*>_N -> <*>_N -> Sym cobox_a3fU)
; Sym (<*>_N -> <*>_N -> Sym
cobox_a3fH))) |> (<*>_N
-> <*>_N
-> Sym
cobox_a3fU)) <a>_N’
Function kind = * -> * -> *
Arg kinds = [(a, TYPE r1)]
}}}
This may be yet another case of the kind of `(->)` being too restrictive
(#11714) since `a -> b` appears to be lifted to the coercion `TyConAppCo
role (->) [a, b]`.
--
--
Ticket URL: