[GHC] #12430: TypeFamilyDependencies accepts invalid injectivity annotation

24 Jul 2016

      #12430: TypeFamilyDependencies accepts invalid injectivity annotation
-------------------------------------+-------------------------------------
           Reporter:  vagarenko      |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider this code (depends on singletons-2.2):

 {{{#!hs
 {-# 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:

 {{{#!hs
 type Foo = Family '[ '(0, 'A), '(1, 'B)]
 type Bar = Family '[ '(0, 'A), '(0, 'B)]
 }}}
 are obviously map to the same type:

 {{{#!hs
 *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:
 {{{#!hs
 type family Family (natList :: NatList) = (r :: Type) | r -> natList where
     Family '[] = ()
     Family xs  = NewType (Map SndSym0 xs)
 }}}
 or change `StripNatList` definition to type family:
 {{{#!hs
 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:
 {{{#!hs
 type family Family (natList :: NatList) = (r :: [Payload]) | r -> natList
 where
     Family xs = StripNatList xs
 }}}
 it fails with correct error regardless of `StripNatList` definition.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12430
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler