[GHC] #9898: Couldn't match type `(Char, ())' with `()'

18 Dec 2014


      #9898: Couldn't match type `(Char, ())' with `()'
-------------------------------------+-------------------------------------
       Reporter:  erisco             |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:  Windows
       Keywords:                     |         Type of failure:  GHC
   Architecture:  x86_64 (amd64)     |  rejects valid program
     Difficulty:  Unknown            |               Test Case:
     Blocked By:                     |                Blocking:
Related Tickets:                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 'test3' is expected to type check given that 'test1' and 'test2' type
 check. 'test4' is not expected to type check.

 {{{
 ghc_bug2.hs:24:9:
     Couldn't match type `(Char, ())' with `()'
     Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())
       Actual type: ()
     In the expression:
         () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
     In an equation for `test2':
         test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

 ghc_bug2.hs:28:9:
     Couldn't match type `(Char, ())' with `()'
     Expected type: Filter (Equal Int) (Char, ())
       Actual type: ()
     In the expression: ()
     In an equation for `test3': test3 = ()
 }}}

 {{{#!hs
 {-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-}
 module Main where

 type family Filter f xs where
   Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs)
   Filter f () = ()
 --

 type family ApplyFilter p xs where
   ApplyFilter False (x, xs) = xs
   ApplyFilter p xs = xs
 --

 type family Equal x y where
   Equal x x = True
   Equal x y = False
 --

 -- Type checks
 test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())
 test1 = ()

 -- Couldn't match type `(Char, ())' with `()'
 test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

 -- Couldn't match type `(Char, ())' with `()'
 test3 :: Filter (Equal Int) (Char, ())
 test3 = ()

 -- Type checks, should not
 test4 :: Filter (Equal Int) (Char, ())
 test4 = ('x', ())
 }}}

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