[Haskell-cafe] type variable is ambiguous in a non-injective type family

[Li-yao Xia]

Hi Henry,

In this context you have:

s :: SubAmbi a

toBool :: Ambi b => SubAmbi b -> Bool

where b is a fresh type variable stemming from the instantiation of 
toBool. When you apply toBool to s, you need to unify (SubAmbi a) and 
(SubAmbi b), however that doesn't unify a and b because SubAmbi is not 
known to be injective. So you don't know that `a` and `b` are equal, and 
so you don't know that `SubAmbi a` and `SubAmbi b` are equal. This 
problem happens whenever, in a function's signature, a type variable 
appears only under type families.

You can resolve the ambiguity by applying toBool explicitly to the type a.

     {-# LANGUAGE ..., ScopedTypeVariables, TypeApplications #-}

                   -- Allow "a" to be referred to in the definition
     whatsWrong :: forall a. Ambi a => a -> IO ()
     whatsWrong = dp
       let s = toSubAmbi a
           b = toBool @a s  -- Instantiate toBool at type "a"
       {- ... -}


Cheers,
Li-yao

On 7/28/19 7:56 AM, Henry Laxen wrote:
> Dear Cafe,
> 
> I really don't understand what is going on here.  I've searched, but I don't
> really understand the links that I found. The closest I've come is:
> 
> https://sulzmann.blogspot.com/2013/01/non-injective-type-functions-and.html
> 
> but I don't understand it enough to see my way to a solution.  Here is a
> minimal example of what I'm trying to do:
> 
> --------------------------------------------------------------------------------
> 
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE AllowAmbiguousTypes #-}
> 
> module Ambiguous where
> 
> class Ambi a where
>    type SubAmbi a :: *
>    toSubAmbi :: a -> SubAmbi a
>    toBool :: SubAmbi a -> Bool
> 
> whatsWrong :: Ambi a => a -> IO ()
> whatsWrong a = do
>    let
>      s = toSubAmbi a
>      b = toBool s
>    if b then print "True" else print "False"
>    
> 
> {-
> 
> src/Games/Ambiguous.hs:15:16: error: …
>      • Couldn't match expected type ‘SubAmbi a0’
>                    with actual type ‘SubAmbi a’
>        NB: ‘SubAmbi’ is a non-injective type family
>        The type variable ‘a0’ is ambiguous
>      • In the first argument of ‘toBool’, namely ‘s’
>        In the expression: toBool s
>        In an equation for ‘b’: b = toBool s
>      • Relevant bindings include
>          s :: SubAmbi a
>            (bound at /home/henry/nadineloveshenry/bin/nlh/src/Games/Ambiguous.hs:14:5)
>          a :: a
>            (bound at /home/henry/nadineloveshenry/bin/nlh/src/Games/Ambiguous.hs:12:12)
>          whatsWrong :: a -> IO ()
>            (bound at /home/henry/nadineloveshenry/bin/nlh/src/Games/Ambiguous.hs:12:1)
>     |
> Compilation failed.
> 
> -}
> --------------------------------------------------------------------------------
> 
> Could any of you Haskell sages please explain how to do this?
> 
> Best wishes,
> Henry Laxen
>