[GHC] #11007: Type family injectivity annotations ignored in hs-boot files

GHC ghc-devs at haskell.org
Thu Oct 22 21:05:05 UTC 2015


#11007: Type family injectivity annotations ignored in hs-boot files
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  7.11
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's the test case:

 {{{
 -- A.hs-boot
 {-# LANGUAGE TypeFamilies #-}

 module A where

 type family Id x = r | r -> x where ..
 }}}

 {{{
 -- needed to avoid illegal self-import
 module B where

 import {-# SOURCE #-} A
 }}}

 {{{
 {-# LANGUAGE TypeFamilies #-}

 module A where

 import B

 type family Id x = r | r -> x where
   Id a = a
 }}}

 I get

 {{{
 A.hs-boot:6:1: error:
     Type constructor ‘Id’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type family Id x = r :: * | r -> x where
                      Id a = a
     Boot file:   type family Id x :: *
 }}}

 Even when declaring an abstract closed type family, it should still be
 able to be injective.

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


More information about the ghc-tickets mailing list