[GHC] #14369: GHC warns an injective type family "may not be injective"

#14369: GHC warns an injective type family "may not be injective" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple InjectiveFamilies | Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14369 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14369: GHC warns an injective type family "may not be injective" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4106 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4106 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14369#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14369: GHC warns an injective type family "may not be injective"
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.2.1
checker) | Keywords:
Resolution: | InjectiveFamilies
Operating System: Unknown/Multiple | Architecture:
Type of failure: Poor/confusing | Unknown/Multiple
error message | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D4106
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott

#14369: GHC warns an injective type family "may not be injective" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: fixed | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Poor/confusing | Test Case: indexed- error message | types/should_fail/T14369 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4106 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => indexed-types/should_fail/T14369 * status: patch => closed * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14369#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC