Skip to content
GitLab
Projects Groups Snippets
  • /
  • 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 5,259
    • Issues 5,259
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 565
    • Merge requests 565
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14720
Closed
Open
Issue created Jan 25, 2018 by Ryan Scott@RyanGlScottMaintainer

GHC 8.4.1-alpha regression with TypeInType

GHC 8.2.2 is able to typecheck this code:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where

import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void

data family Sing (z :: k)

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)

class (PGeneric k, SGeneric k) => VGeneric k where
  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a

data Decision a = Proved a
                | Disproved (a -> Void)

class SDecide k where
  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
  default (%~) :: forall (a :: k) (b :: k). (VGeneric 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) ->
      case (sTof s1, sTof s2) of
          (Refl, Refl) -> Proved Refl
    Disproved contra -> Disproved (\Refl -> contra Refl)

But GHC 8.4.1-alpha2 cannot:

$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics        ( Bug.hs, Bug.o )

Bug.hs:44:52: error:
    • Could not deduce: PFrom a ~ PFrom a
      from the context: b ~ a
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a lambda abstraction
        at Bug.hs:44:37-40
      Expected type: PFrom a :~: PFrom b
        Actual type: PFrom a :~: PFrom a
      NB: ‘PFrom’ is a non-injective type family
    • In the first argument of ‘contra’, namely ‘Refl’
      In the expression: contra Refl
      In the first argument of ‘Disproved’, namely
        ‘(\ Refl -> contra Refl)’
    • Relevant bindings include
        contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
        s2 :: Sing b (bound at Bug.hs:40:9)
        s1 :: Sing a (bound at Bug.hs:40:3)
        (%~) :: Sing a -> Sing b -> Decision (a :~: b)
          (bound at Bug.hs:40:3)
   |
44 |     Disproved contra -> Disproved (\Refl -> contra Refl)
   |                                                    ^^^^
Trac metadata
Trac field Value
Version 8.4.1-alpha1
Type Bug
TypeOfFailure OtherFailure
Priority high
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