GitLab

The following program passes Core Lint on GHC 8.6.3:

{-# 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 (closed) (see #16188 (closed)##16204 (closed)), but this Core Lint error is technically different from the one in that ticket, so I decided to open a new issue for this.

Trac metadata

Trac field	Value
Version	8.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#16188 (closed)
Blocking
CC
Operating system
Architecture