#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