[GHC] #7812: Ambiguity check too eager with unconstrained type variable

[GHC]

#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