[GHC] #9902: Type family, pattern not matching

[GHC]

#9902: Type family, pattern not matching
-------------------------------------+-------------------------------------
       Reporter:  erisco             |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:  MacOS X
       Keywords:                     |         Type of failure:  GHC
   Architecture:  x86_64 (amd64)     |  rejects valid program
     Difficulty:  Unknown            |               Test Case:
     Blocked By:                     |                Blocking:
Related Tickets:                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 This is a follow up to issue #9898. The partially applied type families
 have been eliminated yet type checking is still failing.

 It is expected that 'test1' infer as `(Char, ())` but it does not. It
 seems that GHC is not matching the correct pattern on `:$:`. 'test3' and
 'test4' indicate that GHC sometimes matches the correct pattern.

 'test2' demonstrates an inconsistency between type checking with GHC and
 the type checking that occurs when the same expression is entered in GHCi.
 I do not know if this is a related problem. Enabling AllowAmbiguousTypes
 suggests it might be related because the compiler then complains
 `ApplyFilter (ToBool ((:.:) Not (Equal Char) Char)) (Char, ())` cannot be
 unified with `()` (With the second `:$:` rule enabled).

 Reported type of 'test1' with second rule removed
 {{{
 test1
   :: (Char,
       ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ()))
 }}}

 Reported type of 'test1' with second rule added
 {{{
 test1
   :: (Char,
       ApplyFilter (ToBool ((:.:) Not (Equal Char) Char)) (Char, ()))
 }}}

 test2 type check error
 {{{
 ghc_bug3.hs:38:15:
     Couldn't match expected type ‘ApplyFilter
                                     (ToBool ((Not :.: Equal Char) :$:
 Char)) (Char, ())’
                 with actual type ‘ApplyFilter
                                     (ToBool ((Not :.: Equal Char) :$:
 Char)) (Char, ())’
     NB: ‘ApplyFilter’ is a type function, and may not be injective
     The type variables ‘k0’, ‘k1’, ‘k2’ are ambiguous
     In the ambiguity check for:
       forall (k :: BOX) (k1 :: BOX) (k2 :: BOX).
       ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In an expression type signature:
       ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())
     In the expression:
         () ::
           ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char, ())
 }}}

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

 data Equal x y
 data Not x

 type family ToBool x where
   ToBool (Equal x x) = True
   ToBool (Equal x y) = False
   ToBool (Not True) = False
   ToBool (Not False) = True
   ToBool (Not p) = ToBool (Not (ToBool p))

 data (:.:) g f x
 infixr 9 :.:

 type family f :$: x where
   (g :.: f) :$: x = g (f x)
 -- Uncomment to see change in 'test1' -- f :$: x = f x

 type family Filter f l where
   Filter f (x, xs) = ApplyFilter (ToBool (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 xs :+: ys where
   (x, xs) :+: ys = (x, xs :+: Filter (Not :.: Equal x) ys)
   () :+: ys = ys
 infixl 5 :+:

 test1 = undefined :: (Char, ()) :+: (Char, ())

 -- Typing this into GHCi works fine, but here does not type check.
 test2 = () :: ApplyFilter (ToBool ((Not :.: Equal Char) :$: Char)) (Char,
 ())

 -- Type checks (with second rule added)
 test3 :: Maybe :$: Int
 test3 = Just 5

 -- Type checks
 test4 :: (Maybe :.: Maybe) :$: Int
 test4 = Just (Just 5)
 }}}

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