#15664: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T15664 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
From [https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee... Generic Programming of All Kinds],
{{{#!hs {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
-- https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee...
import Data.Kind import GHC.Exts import Data.Function
data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as)
type family Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where Apply(Type) a E = a Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind -> Ctx(kind) -> Type where A0 :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as -> ApplyT(k -> ks) f (a:&:as)
type f ~> g = (forall xx. f xx -> g xx)
unravel :: ApplyT(k) f ~> Apply(k) f unravel (A0 a) = a unravel (AS fa) = unravel fa }}}
gives a core lint error
{{{ $ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log }}}
New description: From [https://dl.acm.org/citation.cfm?id=3242745 Generic Programming of All Kinds], {{{#!hs {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-} {-# Options_GHC -dcore-lint #-} import Data.Kind import GHC.Exts import Data.Function data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) type family Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where Apply(Type) a E = a Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as data ApplyT kind :: kind -> Ctx(kind) -> Type where A0 :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) as -> ApplyT(k -> ks) f (a:&:as) type f ~> g = (forall xx. f xx -> g xx) unravel :: ApplyT(k) f ~> Apply(k) f unravel (A0 a) = a unravel (AS fa) = unravel fa }}} gives a core lint error {{{ $ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15664#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler