[GHC] #13271: GHC Panic With Injective Type Families

[GHC]

#13271: GHC Panic With Injective Type Families
----------------------------------------+---------------------------------
           Reporter:  wayofthepie       |             Owner:
               Type:  bug               |            Status:  new
           Priority:  normal            |         Milestone:
          Component:  Compiler          |           Version:  8.0.1
           Keywords:                    |  Operating System:  Linux
       Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
          Test Case:                    |        Blocked By:
           Blocking:                    |   Related Tickets:
Differential Rev(s):                    |         Wiki Page:
----------------------------------------+---------------------------------
 The following causes GHC to panic:

 {{{
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilyDependencies #-}

 module T where

 import GHC.TypeLits

 data T1 = T1
 type T2 = TypeError (Text "You can't do that!")

 type family X i = r | r -> i where
   X 1 = T1
   X 2 = T2
 }}}

 {{{
 $ ghc T.hs
 [1 of 1] Compiling T                ( T.hs, T.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.0.1 for x86_64-unknown-linux):
         isInjectiveTyCon sees a TcTyCon T2
 }}}

 This may be related to https://ghc.haskell.org/trac/ghc/ticket/11560.
 Without injectivity it gives the expected type error with the message "You
 can't do that!"
 {{{
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilies #-}

 module T where

 import GHC.TypeLits

 data T1 = T1
 type T2 = TypeError (Text "You can't do that!")

 type family X i where
   X 1 = T1
   X 2 = T2

 }}}
 {{{
 $ ghc T.hs
 [1 of 1] Compiling T                ( T.hs, T.o )

 T.hs:9:1: error:
     • You can't do that
     • In the type synonym declaration for ‘T2’
 }}}
 This isn't something anyone would intentionally write, as it could never
 type check with the type synonym T2 being a TypeError, but a panic is a
 panic so I said I'd raise it anyway.

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