#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: type Resolution: | family, ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jstolarek): For the record, this code can now be compiled using injective type families: {{{#!hs {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} module T9587 where type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *) | r -> repr a b class ESymantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (Arr repr a b) app :: repr (Arr repr a b) -> repr a -> repr b te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x)))) in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) }}} Not sure if that addresses the original problem because: a) `Arr` might not be injective at all b) if I understand correctly [comment:10 comment 10] the actual injectivity annotation on `Arr` is `r repr -> a b` and that is not supported yet -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9587#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler