[GHC] #12113: ghc-8.0.1-rc4: unification false positive?

24 May 2016


      #12113: ghc-8.0.1-rc4: unification false positive?
-------------------------------------+-------------------------------------
           Reporter:  _deepfire      |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1-rc4
           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:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UnicodeSyntax #-}

 module Foo () where

 type family   TF x ∷ *
 data              ADT x
 type instance TF (ADT x) = x

 class (a ~ ADT (TF a)) ⇒ TC2 a b | a → b

 data Forget = ∀ a b. TC2 a b ⇒ Forget a -- ~ Forget (ADT (TF a))

 data PhantomF a b = Constr Forget       -- ~ Constr (Forget (ADT (TF a)))

 f ∷ ∀ a b. TC2 a b ⇒ ADT (TF a) → [Forget]
 f _ = case ((undefined) ∷ (PhantomF a b)) of
         Constr m → [Forget m]

 -- Here GHC 8.0.1-rc4 unifies, whereas GHC 7.10.3 (properly?) fails with:

 -- ghc8-unification-false-positive.hs:20:21:
 --     Couldn't match type ‘Forget’ with ‘ADT (TF Forget)’
 --     In the expression: Forget m
 --     In the expression: [Forget m]
 --     In a case alternative: Constr m -> [Forget m]
 }}}

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