[GHC] #11424: "Occurs check" not considered when reducing closed type families

13 Jan 2016

      #11424: "Occurs check" not considered when reducing closed type families
-------------------------------------+-------------------------------------
           Reporter:  diatchki       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (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:
-------------------------------------+-------------------------------------
 Hello,

 consider the following example:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}

 type family Same a b where
   Same a a = Int
   Same a b = Char

 example :: Same a [a] -> a
 example = undefined

 bad :: a
 bad = example 'c'
 }}}

 This program should type check, using the following reasoning:  `a` and
 `[a]` can never be equal, therefore the first equation for `Same` does not
 apply, and so we can fall trough to the second one, thus reducing `Same`
 to `Char`.   Therefore, `bad` should be accept.

 GHC rejects this program with the following error:
 {{{
    • Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’
     • In the first argument of ‘example’, namely ‘'c'’
       In the expression: example 'c'
       In an equation for ‘bad’: bad = example 'c'
     • Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)
 }}}

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