#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: GHC The Glasgow Haskell Compiler