Type family, pattern not matching
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, ())
{-# 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)
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |