Re: [GHC] #12670: Representation polymorphism validity check is too strict

7 Oct 2016

      #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: <a_a2Xv>_N |> cobox_a2XB ; cobox_a2XC } in
         ...
 }}}
 which produces,
 {{{
 <no location info>: warning:
     In the type ‘((a_a2Xv |> cobox_a2XB) :: *)
                  ~#
                  ((a_a2Xz -> b_a2XA) :: *)’
     Ill-kinded argument in type or kind ‘a_a2Xz -> b_a2XA’
     type or kind ‘a_a2Xz -> b_a2XA’ kind: TYPE r1_a2Xx
 }}}
 due to the fact that `a_a2Xz` has `RuntimeRep`-polymorphic kind `TYPE
 r1_a2Xx`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12670#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler