#12670: Representation polymorphism validity check is too strict
-------------------------------------+-------------------------------------
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:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by bgamari):
It seems that the above validity check loosening would also require that
the Core Linter be loosened a bit. Otherwise, we find that this program
will typecheck yet then fail due to validity check errors,
{{{#!hs{-# LANGUAGE TypeInType, PolyKinds, GADTs, RankNTypes #-}
module Hi where
import GHC.Exts
data Fingerprint = Fingerprint
data TyCon = TyCon
data TypeRep (a :: k) where
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
Fingerprint
-> TypeRep a
-> TypeRep b
-> TypeRep (a -> b)
data AppResult (t :: k) where
App :: TypeRep a -> TypeRep b -> AppResult (a b)
splitApp :: TypeRep a -> Maybe (AppResult a)
splitApp (TrFun _ _ _) = Nothing
}}}
The Core lint issues stem from the fact that we have number of (unused)
coercion bindings in scope in the produced Core whose types fail the
`okArrowArgKind` check performed by `lintArrow`. For instance,
{{{#!hs
splitApp :: forall k_a2Xm (a_a2VN :: k_a2Xm).
TypeRep k_a2Xm a_a2VN -> Maybe (AppResult k_a2Xm a_a2VN)
splitApp =
\ (@ k_a2Xu)
(@ (a_a2Xv :: k_a2Xu))
(ds_d37A :: TypeRep k_a2Xu a_a2Xv) ->
case ds_d37A of wild_00
{ TrFun @ r1_a2Xx @ r2_a2Xy @ a_a2Xz @ b_a2XA
cobox_a2XB cobox_a2XC
ds_d37Y ds_d37Z ds_d380 ->
...
let {
cobox_a2XU :: ((a_a2Xv |> cobox_a2XB) :: *) ~# ((a_a2Xz ->
b_a2XA) :: *)
cobox_a2XU = CO: