[GHC] #14556: Core Lint error: Ill-kinded result in coercion
#14556: Core Lint error: Ill-kinded result in coercion -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #14554 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} import Data.Kind import Data.Proxy data Fn a b where IdSym :: Fn Type Type type family (@@) (f::Fn k k') (a::k)::k' where IdSym @@ a = a data KIND = X | FNARR KIND KIND data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' data TyRep (kind::KIND) :: TY kind -> Type where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) type family IK (kind::KIND) :: Type where IK X = Type IK (FNARR k k') = Fn (IK k) (IK k') type family IT (ty::TY kind) :: IK kind where IT ID = IdSym IT (FNAPP f x) = IT f @@ IT x zero :: TyRep X a -> IT a zero = undefined }}} which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore- lint` (8.3.20171122) attached. It compiles fine with {{{#!hs zero :: TyRep X a -> IT a zero = zero }}} but fails with `zero = let x = x in x`. See #14554. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14556 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14556: Core Lint error: Ill-kinded result in coercion -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14554 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "bug.log" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14556 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14556: Core Lint error: Ill-kinded result in coercion -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14554 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I think this is another example of the bugs surrounding "flattened types have flattened kinds". What is happening is this. In the RHS of `zero` we get a constraint {{{ [W} (alpha :: TYPE r) ~ TyRep X a -> (IT a |> ax_IK) where ax_IK :: IK X ~ Type -- Just an axiom for IK }}} which should strainghtforwardly unify. But before we do that we flatten `(IT a |> ax_IK)`, but alas we get just {{{ (fuv :: IK X) where fuv = IT a -- CFunEqCan }}} The cast has disappeared. This happens in `TcFlatten`: {{{ flatten_one (CastTy ty g) }}} I'm pretty sure it's just another manifestation of our existing set of bugs around flattening (Trac #12919). Richard has a mostly- finished patch that cures this --- it'd be great to get it finished! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14556#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14556: Core Lint error: Ill-kinded result in coercion
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.3
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #14554 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#14556: Core Lint error: Ill-kinded result in coercion -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_compile/T14556 Blocked By: | Blocking: Related Tickets: #14554 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => dependent/should_compile/T14556 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14556#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC