Re: [GHC] #14162: Core Lint error

28 Aug 2017

      #14162: Core Lint error
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeInType
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 simonpj):

 But the actual error is somewhere in the unfolding wrapper for `SSubNil`,
 which is injected by `CorePrep` and looks like this
 {{{
 SSubNil
   :: forall a (ys :: Maybe a) (x :: SubList a ys).
      ((ys :: Maybe a) ~# ('Nothing a :: Maybe a),
       (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing a))) =>
      R:SingSubListx a ys x
 [GblId[DataCon],
  Arity=2,
  Caf=NoCafRefs,
  Str=<L,U><L,U>m,
  Unf=OtherCon []]
 SSubNil
   = \ (@ a_aSK)
       (@ (ys_aRV :: Maybe a_aSK))
       (@ (x_aRW :: SubList a_aSK ys_aRV))
       (eta_B2
          :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK))
       (eta_B1
          :: (x_aRW :: SubList a_aSK ys_aRV)
             ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK))) ->
       SSubNil
         @ a_aSK
         @ ys_aRV
         @ x_aRW
         @~ (eta_B2
             :: (ys_aRV :: Maybe a_aSK) ~# ('Nothing a_aSK :: Maybe a_aSK))
         @~ (eta_B1
             :: (x_aRW :: SubList a_aSK ys_aRV)
                ~# ('SubNil a_aSK :: SubList a_aSK ('Nothing a_aSK)))
 }}}
 Lint says
 {{{
 *** Core Lint errors : in result of CorePrep ***
 <no location info>: warning:
     In the type ‘forall a (ys :: Maybe a) (x :: SubList a ys).
                  ((ys :: Maybe a) ~# ('Nothing a :: Maybe a),
                   (x :: SubList a ys) ~# ('SubNil a :: SubList a ('Nothing
 a))) =>
                  R:SingSubListx a ys x’
     Kind application error in type ‘SubList a_aSK ys_aRV’
       Function kind = forall {a}. Maybe a -> *
       Arg kinds = [(a_aSK, *), (ys_aRV, Maybe a_aSv)]
 }}}

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