[GHC] #16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type)

19 Jan 2019

      #16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.7
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #16188
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program passes Core Lint on GHC 8.6.3:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 import Data.Kind

 -----
 -- singletons machinery
 -----

 data family Sing :: forall k. k -> Type
 data SomeSing :: Type -> Type where
   SomeSing :: Sing (a :: k) -> SomeSing k

 -----
 -- (Simplified) GHC.Generics
 -----

 class Generic (a :: Type) where
     type Rep a :: Type
     from :: a -> Rep a
     to   :: Rep a -> a

 class PGeneric (a :: Type) where
   -- type PFrom ...
   type PTo (x :: Rep a) :: a

 class SGeneric k where
   -- sFrom :: ...
   sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)

 -----

 class SingKind k where
   type Demote k :: Type
   -- fromSing :: ...
   toSing :: Demote k -> SomeSing k

 genericToSing :: forall k.
                  ( SingKind k, SGeneric k, SingKind (Rep k)
                  , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
               => Demote k -> SomeSing k
 genericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo

 withSomeSing :: forall k r
               . SingKind k
              => Demote k
              -> (forall (a :: k). Sing a -> r)
              -> r
 withSomeSing x f =
   case toSing x of
     SomeSing x' -> f x'
 }}}

 But not on GHC HEAD:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Desugar (before optimization) ***
 <no location info>: warning:
     In the expression: $ @ 'LiftedRep
                          @ (forall (a :: Rep k_a1cV). Sing a -> SomeSing
 k_a1cV)
                          @ (SomeSing k_a1cV)
                          (withSomeSing
                             @ (Rep k_a1cV)
                             @ (SomeSing k_a1cV)
                             $dSingKind_a1d5
                             ((from
                                 @ (Demote k_a1cV)
                                 $dGeneric_a1d7
                                 (d_aX7
                                  `cast` (Sub co_a1dK
                                          :: Demote k_a1cV[sk:1] ~R# Demote
 k_a1cV[sk:1])))
                              `cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM)
 ; (Sym co_a1dQ ; (Demote
 (Sym co_a1dO))_N))
                                      :: Rep (Demote k_a1cV[sk:1]) ~R#
 Demote (Rep k_a1cV[sk:1]))))
                          (\ (@ (a_a1dc :: Rep k_a1cV)) ->
                             let {
                               $dSGeneric_a1dm :: SGeneric k_a1cV
                               [LclId]
                               $dSGeneric_a1dm = $dSGeneric_a1cY } in
                             . @ (Sing (PTo Any))
                               @ (SomeSing k_a1cV)
                               @ (Sing Any)
                               (SomeSing @ k_a1cV @ (PTo Any))
                               ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
                                `cast` (Sym (Sing
                                               (Sym co_a1dO) (Sym (GRefl
 nominal Any co_a1dO)))_R
                                        ->_R <Sing (PTo Any)>_R
                                        :: (Sing Any -> Sing (PTo Any))
                                           ~R# (Sing Any -> Sing (PTo
 Any)))))
     Argument value doesn't match argument type:
     Fun type:
         (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)
         -> SomeSing k_a1cV
     Arg type: forall (a :: Rep k_a1cV). Sing Any -> SomeSing k_a1cV
     Arg:
         \ (@ (a_a1dc :: Rep k_a1cV)) ->
           let {
             $dSGeneric_a1dm :: SGeneric k_a1cV
             [LclId]
             $dSGeneric_a1dm = $dSGeneric_a1cY } in
           . @ (Sing (PTo Any))
             @ (SomeSing k_a1cV)
             @ (Sing Any)
             (SomeSing @ k_a1cV @ (PTo Any))
             ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
              `cast` (Sym (Sing
                             (Sym co_a1dO) (Sym (GRefl nominal Any
 co_a1dO)))_R
                      ->_R <Sing (PTo Any)>_R
                      :: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any -> Sing
 (PTo Any))))
 *** Offending Program ***
 <elided>
 genericToSing
   :: forall k.
      (SingKind k, SGeneric k, SingKind (Rep k), Generic (Demote k),
       Rep (Demote k) ~ Demote (Rep k)) =>
      Demote k -> SomeSing k
 [LclIdX]
 genericToSing
   = \ (@ k_a1cV)
       ($dSingKind_a1cX :: SingKind k_a1cV)
       ($dSGeneric_a1cY :: SGeneric k_a1cV)
       ($dSingKind_a1cZ :: SingKind (Rep k_a1cV))
       ($dGeneric_a1d0 :: Generic (Demote k_a1cV))
       ($d~_a1d1 :: Rep (Demote k_a1cV) ~ Demote (Rep k_a1cV)) ->
       let {
         co_a1dQ :: Demote (Rep k_a1cV) ~# Demote (Rep k_a1cV)
         [LclId[CoVarId]]
         co_a1dQ = CO: <Demote (Rep k_a1cV)>_N } in
       let {
         co_a1dO :: Rep k_a1cV ~# Rep k_a1cV
         [LclId[CoVarId]]
         co_a1dO = CO: <Rep k_a1cV>_N } in
       let {
         $dSingKind_a1dT :: SingKind (Rep k_a1cV)
         [LclId]
         $dSingKind_a1dT
           = $dSingKind_a1cZ
             `cast` (Sub (Sym (SingKind (Sym co_a1dO))_N)
                     :: SingKind (Rep k_a1cV[sk:1])
                        ~R# SingKind (Rep k_a1cV[sk:1])) } in
       let {
         $dSingKind_a1d5 :: SingKind (Rep k_a1cV)
         [LclId]
         $dSingKind_a1d5
           = $dSingKind_a1dT
             `cast` ((SingKind (Sym co_a1dO))_R
                     :: SingKind (Rep k_a1cV[sk:1])
                        ~R# SingKind (Rep k_a1cV[sk:1])) } in
       let {
         co_a1dM :: Rep (Demote k_a1cV) ~# Rep (Demote k_a1cV)
         [LclId[CoVarId]]
         co_a1dM = CO: <Rep (Demote k_a1cV)>_N } in
       let {
         co_a1dK :: Demote k_a1cV ~# Demote k_a1cV
         [LclId[CoVarId]]
         co_a1dK = CO: <Demote k_a1cV>_N } in
       let {
         $dGeneric_a1dU :: Generic (Demote k_a1cV)
         [LclId]
         $dGeneric_a1dU
           = $dGeneric_a1d0
             `cast` (Sub (Sym (Generic (Sym co_a1dK))_N)
                     :: Generic (Demote k_a1cV[sk:1])
                        ~R# Generic (Demote k_a1cV[sk:1])) } in
       let {
         $dGeneric_a1d7 :: Generic (Demote k_a1cV)
         [LclId]
         $dGeneric_a1d7 = $dGeneric_a1dU } in
       case eq_sel
              @ * @ (Rep (Demote k_a1cV)) @ (Demote (Rep k_a1cV)) $d~_a1d1
       of co_a1dI
       { __DEFAULT ->
       let {
         co_a1dR :: Rep (Demote k_a1cV) ~# Demote (Rep k_a1cV)
         [LclId[CoVarId]]
         co_a1dR
           = CO: ((Sym co_a1dM ; (Rep
                                    (Sym co_a1dK))_N) ; co_a1dI) ; Sym (Sym
 co_a1dQ ; (Demote
 (Sym co_a1dO))_N) } in
       \ (d_aX7 :: Demote k_a1cV) ->
         $ @ 'LiftedRep
           @ (forall (a :: Rep k_a1cV). Sing a -> SomeSing k_a1cV)
           @ (SomeSing k_a1cV)
           (withSomeSing
              @ (Rep k_a1cV)
              @ (SomeSing k_a1cV)
              $dSingKind_a1d5
              ((from
                  @ (Demote k_a1cV)
                  $dGeneric_a1d7
                  (d_aX7
                   `cast` (Sub co_a1dK
                           :: Demote k_a1cV[sk:1] ~R# Demote
 k_a1cV[sk:1])))
               `cast` (Sub (Sym (Sym co_a1dR ; Sym co_a1dM) ; (Sym co_a1dQ
 ; (Demote
 (Sym co_a1dO))_N))
                       :: Rep (Demote k_a1cV[sk:1]) ~R# Demote (Rep
 k_a1cV[sk:1]))))
           (\ (@ (a_a1dc :: Rep k_a1cV)) ->
              let {
                $dSGeneric_a1dm :: SGeneric k_a1cV
                [LclId]
                $dSGeneric_a1dm = $dSGeneric_a1cY } in
              . @ (Sing (PTo Any))
                @ (SomeSing k_a1cV)
                @ (Sing Any)
                (SomeSing @ k_a1cV @ (PTo Any))
                ((sTo @ k_a1cV $dSGeneric_a1dm @ Any)
                 `cast` (Sym (Sing
                                (Sym co_a1dO) (Sym (GRefl nominal Any
 co_a1dO)))_R
                         ->_R <Sing (PTo Any)>_R
                         :: (Sing Any -> Sing (PTo Any)) ~R# (Sing Any ->
 Sing (PTo Any)))))
       }
 }}}

 I'm not sure if this is related to #16188 (see
 https://ghc.haskell.org/trac/ghc/ticket/16188#comment:1), but this Core
 Lint error is technically different from the one in that ticket, so I
 decided to open a new issue for this.

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