Opened 2 years ago

Closed 2 years ago

#14369 closed bug (fixed)

GHC warns an injective type family "may not be injective"

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: InjectiveFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: indexed-types/should_fail/T14369
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4106
Wiki Page:

Description

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

data family Sing (a :: k)

data instance Sing (z :: Maybe a) where
  SNothing :: Sing Nothing
  SJust :: Sing x -> Sing (Just x)

class SingKind k where
  type Demote k = r | r -> k
  fromSing :: Sing (a :: k) -> Demote k

instance SingKind a => SingKind (Maybe a) where
  type Demote (Maybe a) = Maybe (Demote a)
  fromSing SNothing = Nothing
  fromSing (SJust x) = Just (fromSing x)

f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:26:5: error:
    • Couldn't match type ‘Demote a’ with ‘Demote a1’
      Expected type: Sing (x a) -> Maybe (Demote a1)
        Actual type: Sing (x a) -> Demote (Maybe a)
      NB: ‘Demote’ is a type function, and may not be injective
    • In the expression: fromSing
      In an equation for ‘f’: f = fromSing
    • Relevant bindings include
        f :: Sing (x a) -> Maybe (Demote a1) (bound at Bug.hs:26:1)
   |
26 | f = fromSing
   |     ^^^^^^^^

That NB: ‘Demote’ is a type function, and may not be injective suggestion shouldn't be shown here, since Demote is definitely injective.

Change History (3)

comment:1 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D4106
Status: newpatch

comment:2 Changed 2 years ago by Ryan Scott <ryan.gl.scott@…>

In 8846a7fd/ghc:

Fix #14369 by making injectivity warnings finer-grained

Summary:
Previously, GHC would always raise the possibility that a
type family might not be injective in certain error messages, even if
that type family actually //was// injective. Fix this by actually
checking for a type family's lack of injectivity before emitting
such an error message.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #14369

Differential Revision: https://phabricator.haskell.org/D4106

comment:3 Changed 2 years ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: indexed-types/should_fail/T14369
Note: See TracTickets for help on using tickets.