Opened 3 years ago

Closed 11 months ago

#12430 closed bug (fixed)

TypeFamilyDependencies accepts invalid injectivity annotation

Reported by: vagarenko Owned by:
Priority: high Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: InjectiveFamilies Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5228
Wiki Page:

Description

Consider this code (depends on singletons-2.2):

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,
KindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-}

module Bug where

import Data.Kind (Type)
import Data.Singletons.Prelude (Map, SndSym0)
import GHC.TypeLits (Nat)

data Payload = A | B

newtype NewType a = NewType Int

type NatList = [(Nat, Payload)]

type StripNatList (natList :: NatList) = Map SndSym0 natList

type family Family (natList :: NatList) = (r :: Type) | r -> natList where
    Family '[] = ()
    Family xs  = NewType (StripNatList xs)    

Why GHC is okay with injectivity annotation for Family: r -> natList?

These two types:

type Foo = Family '[ '(0, 'A), '(1, 'B)]
type Bar = Family '[ '(0, 'A), '(0, 'B)]

are obviously map to the same type:

*Bug Data.Singletons.Prelude> :kind! Foo
Foo :: *
= NewType ('A :$$$ '['B])
*Bug Data.Singletons.Prelude> :kind! Bar
Bar :: *
= NewType ('A :$$$ '['B])

If inline StripNatList inside Family definition:

type family Family (natList :: NatList) = (r :: Type) | r -> natList where
    Family '[] = ()
    Family xs  = NewType (Map SndSym0 xs)

or change StripNatList definition to type family:

type family StripNatList (natList :: NatList) where
    StripNatList '[] = '[]
    StripNatList ('(n, x) ': xs) = x ': StripNatList xs

compilation expectedly fails with Type family equation violates injectivity annotation.


Moreover, if I remove NewType from Family and change result kind:

type family Family (natList :: NatList) = (r :: [Payload]) | r -> natList where
    Family xs = StripNatList xs

it fails with correct error regardless of StripNatList definition.

Change History (6)

comment:1 Changed 3 years ago by goldfire

It looks like we're not being aggressive enough in unrolling type synonyms -- a legitimate bug.

comment:2 Changed 11 months ago by monoidal

Here's a simpler version:

{-# LANGUAGE TypeFamilies, PolyKinds, KindSignatures, TypeFamilyDependencies,
GADTs, ScopedTypeVariables #-}

module Bug where

import Data.Kind (Type)

data Proxy a

type C a = Int

type family Family (x :: Type) = (y :: Type) | y -> x where
    Family x  = Proxy (C x)

Family shouldn't be allowed to be injective, it's a constant function: Family Int ~ Family Bool.

comment:3 Changed 11 months ago by RyanGlScott

Keywords: InjectiveFamilies added

Even simpler:

{-# LANGUAGE TypeFamilyDependencies #-}
module Bug where

type C a = Int
type family F x = y | y -> x where
  F x = C x

I'm on this.

comment:4 Changed 11 months ago by RyanGlScott

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

comment:5 Changed 11 months ago by Ben Gamari <ben@…>

In 26e81e90/ghc:

Fix #12430 by expanding type synonyms in injTyVarsOfType

We weren't expanding type synonyms when determining the
injective type variables of a type, leading to certain non-injective
families being mistakenly labeled as injective (#12430). Easily fixed
with a tactical use of `coreView`.

Test Plan: make test TEST=T12430

Reviewers: bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, carter

GHC Trac Issues: #12430

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

comment:6 Changed 11 months ago by bgamari

Milestone: 8.8.1
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.