#7812: Ambiguity check too eager with unconstrained type variable ----------------------------------------+----------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Keywords: AmbiguityCheck | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by goldfire): I understand the motivation for disallowing my code, but perhaps I have a compelling enough use case to counter that argument. I'm experimenting with heterogeneous lists, using the HList library as a high-level design spec, but I'm avoiding any use of functional dependencies in my code. The HList library defines {{{hMapOut}}}, a function to map a hetero list to a plain old regular list. Because the function involved in the map must work with a variety of types of input (because the source list is hetero), HList uses a symbol to represent the function and defines instances of a class (which I call {{{Applicable}}}) to define the operation of the function at different types. {{{ class Applicable (f :: *) (x :: *) where type Apply f x :: * apply :: f -> x -> Apply f x -- example to aid understanding of Applicable; otherwise, Id is unused here data Id = Id instance Applicable Id x where type Apply Id x = x apply Id x = x }}} Here is my definition of hetero lists: {{{ data HList :: [*] -> * where HNil :: HList '[] HCons :: h -> HList t -> HList (h ': t) }}} How can we define {{{hMapOut}}}? Provided we are mapping over a non-empty list, we can simply use the {{{Apply}}} associated type family on, say, the first type in the list to find the resultant type. But, what should we do on an empty list? Ideally, we want the type of {{{hMapOut f HNil}}} to be {{{[a]}}} for any {{{a}}}. But, it is necessary to define {{{hMapOut}}} to use a type family in its return type, and thus the return type of {{{hMapOut}}} looks like the return type of {{{foo}}}, above -- it mentions a type variable that is not mentioned anywhere else in the type. Here are my definitions, which work well under GHC 7.6.1: {{{ type family MapOut (f :: *) (list :: [*]) (a :: *) :: * type instance MapOut f '[] a = a type instance MapOut f (h ': t) a = Apply f h type family MapOuttable (f :: *) (list :: [*]) :: Constraint type instance MapOuttable f '[] = () type instance MapOuttable f '[elt] = Applicable f elt type instance MapOuttable f (h1 ': h2 ': t) = (Applicable f h1, Apply f h1 ~ Apply f h2, MapOuttable f (h2 ': t)) data Proxy a = P hMapOutP :: MapOuttable f list => Proxy a -> f -> HList list -> [MapOut f list a] hMapOutP _ _ HNil = [] hMapOutP _ f (HCons elt HNil) = [apply f elt] hMapOutP p f (HCons h t@(HCons _ _)) = apply f h : hMapOutP p f t hMapOut :: forall f list a. MapOuttable f list => f -> HList list -> [MapOut f list a] hMapOut = hMapOutP (P :: Proxy a) }}} Unsurprisingly, my {{{hMapOutP}}} function needs a {{{Proxy}}} argument, because it is recursive and needs to make sure that the result type is consistent across recursive calls. But, the toplevel {{{hMapOut}}} function does not need a proxy, and it works as desired, allowing {{{a}}} to be inferred for an empty list. An alternate design for this would have each function symbol (like {{{Id}}}) to declare a ''default'' type, just for this scenario. Then, we would have an escape hatch for the empty list. But, that won't always be possible. Consider a symbol {{{Widen}}} that maps both {{{Int}}}s and {{{Integer}}}s to {{{Integer}}}s and maps both {{{Float}}}s and {{{Double}}}s to {{{Double}}}s. This seems like a logical enough operation, and yet it would resist a default type. I think a reasonable person could look at all of this and say "Well, yes, but it's all quite a strange corner case and not something we need to support". I couldn't strongly disagree with such a statement. But, I don't see another way, without functional dependencies, of getting this behavior. One possible way to support this code would be to have a new language flag (ugh) to disable the new ambiguity check. That would restore the GHC 7.6.1 behavior and would suffice for my needs. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7812#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler