[GHC] #15664: Core Lint error
GHC
ghc-devs at haskell.org
Fri Sep 21 21:11:53 UTC 2018
#15664: Core Lint error
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.6.1-beta1
Keywords: TypeInType | Operating System: Unknown/Multiple
Architecture: | Type of failure: None/Unknown
Unknown/Multiple |
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
From
[https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee5a322b6cdd1e45355db16a30d8af/data/hask2018_draft.pdf
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/845e74b59aee5a322b6cdd1e45355db16a30d8af/data/hask2018_draft.pdf
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>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list