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