Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,842
    • Issues 4,842
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 457
    • Merge requests 457
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15346

Closed
Open
Created Jul 05, 2018 by Ryan Scott@RyanGlScottMaintainer

Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression

The following program typechecks on GHC 8.6.1-alpha1:

{-# 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])
Trac metadata
Trac field Value
Version 8.5
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking