#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