ghc-tickets

Download

ghc-tickets@haskell.org

August 2018

1 participants
761 discussions

[GHC] #15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression
by GHC 01 Aug '18

01 Aug '18

#15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (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: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program typechecks on GHC 8.6.1-alpha1: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module SGenerics where import Data.Kind import Data.Type.Equality import Data.Void ----- -- singletons machinery ----- data family Sing :: forall k. k -> Type data instance Sing :: () -> Type where STuple0 :: Sing '() type Refuted a = a -> Void data Decision a = Proved a | Disproved (Refuted a) ----- -- A stripped down version of GHC.Generics ----- data U1 = MkU1 data instance Sing (z :: U1) where SMkU1 :: Sing MkU1 ----- class Generic (a :: Type) where type Rep a :: Type from :: a -> Rep a to :: Rep a -> a class PGeneric (a :: Type) where type PFrom (x :: a) :: Rep a type PTo (x :: Rep a) :: a class SGeneric k where sFrom :: forall (a :: k). Sing a -> Sing (PFrom a) sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k) sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a ----- instance Generic () where type Rep () = U1 from () = MkU1 to MkU1 = () instance PGeneric () where type PFrom '() = MkU1 type PTo 'MkU1 = '() instance SGeneric () where sFrom STuple0 = SMkU1 sTo SMkU1 = STuple0 sTof STuple0 = Refl sFot SMkU1 = Refl ----- class SDecide k where -- | Compute a proof or disproof of equality, given two singletons. (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k)) => Sing a -> Sing b -> Decision (a :~: b) s1 %~ s2 = case sFrom s1 %~ sFrom s2 of Proved (Refl :: PFrom a :~: PFrom b) -> let r :: PTo (PFrom a) :~: PTo (PFrom b) r = Refl sTof1 :: PTo (PFrom a) :~: a sTof1 = sTof s1 sTof2 :: PTo (PFrom b) :~: b sTof2 = sTof s2 in Proved (sym sTof1 `trans` r `trans` sTof2) Disproved contra -> Disproved (\Refl -> contra Refl) instance SDecide U1 where SMkU1 %~ SMkU1 = Proved Refl instance SDecide () }}} However, it throws a Core Lint error with `-dcore-lint`. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit: {{{ *** Core Lint errors : in result of Simplifier *** <no location info>: warning: In the expression: <elided> From-type of Cast differs from type of enclosed expression From-type: U1 Type of enclosed expr: Rep () Actual enclosed expr: PFrom a_a1Fm Coercion used in cast: Sym (D:R:Rep()[0]) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 15

Jump to page: