[GHC] #16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type)
#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
#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 (Type | Version: 8.7 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (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): {{{#!hs 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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 (Type | Version: 8.7 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (by monoidal): I simplified to: {{{ #!haskell {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module T16204 where import Data.Kind data family Sing :: forall k. k -> Type type family Rep (a :: Type) :: Type type family PTo (x :: Rep a) :: a sTo :: forall (k :: Type) (a :: Rep k). (Sing a, Sing (PTo a :: k)) sTo = sTo x :: forall (a :: Type). Sing a x = fst sTo }}} This program is rejected (IMO correctly) by 8.6, but gives Core Lint error in HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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 (Type | Version: 8.7 checker) | Resolution: | 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, #16225 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #16188 => #16188, #16225 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Resolution: | 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, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T16204{a,b}, | typecheck/should_fail/T16204c Blocked By: | Blocking: Related Tickets: #16188, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => merge * testcase: => typecheck/should_compile/T16204{a,b}, typecheck/should_fail/T16204c Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/4a4ae70f09009c5d32696445a06eacb273... 4a4ae70f09009c5d32696445a06eacb273f364b5]. Please merge this into 8.8. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16204: GHC HEAD-only Core Lint error (Argument value doesn't match argument type) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T16204{a,b}, | typecheck/should_fail/T16204c Blocked By: | Blocking: Related Tickets: #16188, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Comment (by Marge Bot <ben+marge-bot@…>): In [changeset:"4a4ae70f09009c5d32696445a06eacb273f364b5/ghc" 4a4ae70/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="4a4ae70f09009c5d32696445a06eacb273f364b5" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16204#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC