#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 _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 _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: _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: _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 _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