Opened 9 months ago

Last modified 8 months ago

#16204 merge bug

GHC HEAD-only Core Lint error (Argument value doesn't match argument type)

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: typecheck/should_compile/T16204{a,b}, typecheck/should_fail/T16204c
Blocked By: Blocking:
Related Tickets: #16188, #16225 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/207
Wiki Page:

Description

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 (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.

Change History (6)

comment:1 Changed 9 months ago by RyanGlScott

This isn't even the only issue with this program that's surfaced on GHC HEAD. If you use this slightly modified version of genericToSing (the only difference is that the explicit @(Rep k) argument has been removed):

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 (from d) $ SomeSing . sTo

Then GHC 8.6.3 compiles it successfully, whereas GHC HEAD gives a strange error:

$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:49:33: error:
    • Could not deduce: Demote k0 ~ Demote (Rep k)
      from the context: (SingKind k, SGeneric k, SingKind (Rep k),
                         Generic (Demote k), Rep (Demote k) ~ Demote (Rep k))
        bound by the type signature for:
                   genericToSing :: forall k.
                                    (SingKind k, SGeneric k, SingKind (Rep k), Generic (Demote k),
                                     Rep (Demote k) ~ Demote (Rep k)) =>
                                    Demote k -> SomeSing k
        at Bug.hs:(45,1)-(48,39)
      Expected type: Demote k0
        Actual type: Rep (Demote k)
      NB: ‘Demote’ is a non-injective type family
      The type variable ‘k0’ is ambiguous
    • In the first argument of ‘withSomeSing’, namely ‘(from d)’
      In the expression: withSomeSing (from d)
      In the expression: withSomeSing (from d) $ SomeSing . sTo
    • Relevant bindings include
        d :: Demote k (bound at Bug.hs:49:15)
        genericToSing :: Demote k -> SomeSing k (bound at Bug.hs:49:1)
   |
49 | genericToSing d = withSomeSing (from d) $ SomeSing . sTo
   |                                 ^^^^^^

It's unclear to me if this issue is the same as the one causing the Core Lint error or not.

comment:2 Changed 9 months ago by monoidal

I simplified to:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module T16204 where

import Data.Kind

data family Sing :: forall k. k -> Type
type family Rep  :: Type

sTo :: forall (a :: Rep). Sing a
sTo = sTo

x :: forall (a :: Type). Sing a
x = id sTo

This program is rejected (correctly) by 8.6, but gives Core Lint error in HEAD.

Last edited 9 months ago by monoidal (previous) (diff)

comment:3 Changed 9 months ago by RyanGlScott

comment:4 Changed 9 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/207
Status: newpatch

comment:5 Changed 8 months ago by RyanGlScott

Status: patchmerge
Test Case: typecheck/should_compile/T16204{a,b}, typecheck/should_fail/T16204c

Landed in 4a4ae70f09009c5d32696445a06eacb273f364b5.

Please merge this into 8.8.

comment:6 Changed 8 months ago by Marge Bot <ben+marge-bot@…>

In 4a4ae70/ghc:

Fix #16188

There was an awful lot of zipping going on in
canDecomposableTyConAppOK, and one of the lists being zipped
was too short, causing the result to be too short. Easily
fixed.

Also fixes #16204 and #16225

test case: typecheck/should_compile/T16188
           typecheck/should_compile/T16204[ab]
           typecheck/should_fail/T16204c
           typecheck/should_compile/T16225
Note: See TracTickets for help on using tickets.