CODEWITHSUNDEEP
haskelltypestypeclassambiguous
dbanas
dbanas

Reputation: 1898

How do I avoid ambiguous type errors in generic functions on typeclasses, in Haskell?

I'm trying to write a universal function for a typeclass:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

module Foo1 where

import Data.Foldable

class Foo t where
  type FooPType t :: *              -- Base type.
  type FooFType t :: * -> *         -- Container type.
  defPs :: FooFType t (FooPType t)  -- Initialized container.

-- An attempt at a universal testing function valid for all types, t,
-- of class Foo for which `FooFType t` is a foldable functor.
tst :: forall t.
  ( Foo t
  , Functor  (FooFType t)
  , Foldable (FooFType t)
  ) => FooPType t
tst = (head . toList) defPs

But, I'm getting this error from GHC (8.0.2):

Foo1.hs:30:23: error:
    • Couldn't match type ‘FooPType t0’ with ‘FooPType t’
      Expected type: FooFType t0 (FooPType t)
        Actual type: FooFType t0 (FooPType t0)
      NB: ‘FooPType’ is a type function, and may not be injective
      The type variable ‘t0’ is ambiguous
    • In the first argument of ‘head . toList’, namely ‘defPs’
      In the expression: (head . toList) defPs
      In an equation for ‘tst’: tst = (head . toList) defPs
    • Relevant bindings include
        tst :: FooPType t (bound at Foo1.hs:30:1)

Poking around a bit, I found that some people have gotten around this problem by changing "type" to "data", but this didn't work for me. (I changed it for FooFType. Should I have changed it for FooPType? For both?)

D'oh! I should've tried answering that last question myself, before posting. Sure enough, changing this line of code:

  type FooPType t :: *              -- Base type.

to read:

  data FooPType t :: *              -- Base type.

got rid of my compile error.

Can anyone explain why that change worked?

Here is the solution, as per @HTNW 's tip, re: adding "@t" after "defPs":

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Foo1 where

import Data.Foldable

class Foo t where
  type FooPType t :: *              -- Base type.
  type FooFType t :: * -> *         -- Container type.
  defPs :: FooFType t (FooPType t)  -- Initialized container.

-- An attempt at a universal testing function valid for all types of class Foo.
tst :: forall t.
  ( Foo t
  , Functor  (FooFType t)
  , Foldable (FooFType t)
  ) => FooPType t
tst = (head . toList) $ defPs @t

The code above compiles w/o error under GHC 8.0.2:

Davids-Air-2:so_noninjective_type_funcs dbanas$ stack ghc -- -c Foo1.hs 

Davids-Air-2:so_noninjective_type_funcs dbanas$

Upvotes: 0

Views: 131

Answers (1)

HTNW
HTNW

Reputation: 29193

tst :: forall t. _ => FooPType t
tst = head $ toList _ -- want f (FooPType t)
defPs :: FooFType u (FooPType u)
tst = head $ toList defPs
-- try to unify (f (FooPType t)) with
--   (FooFType u (FooPType u))
-- Assume that f is injective: f x ~ g y iff f ~ g and x ~ y
-- GHC assumes this because it doesn't allow you to abstract over non-injective
--   type constructors anyway.
-- try to unify f with FooFType u; OK
-- try to unify FooPType t with FooPType u; oops

If FooPType is a data family, then FooPType x ~ FooPType y means x ~ y, because data familys are injective. Here, it's just a type family, which means that the compiler cannot infer that you want to call defPs for the type t. You could, for example, add FooPType u ~ FooPType t to test's context, and now both u and t are valid type arguments to defPs.

test :: forall t u.
        (  Foo t, Foo u
         , Foldable (FooFType t), Foldable (FooFType u)
         , FooPType t ~ FooPType u
        ) => FooPType u
test = head $ toList defPs -- uh oh; which one?

instance Foo Bool where
  type FooPType Bool = Int
  type FooFType Bool = []
  defPs = [1]
instance Foo Int where
  type FooPType Int = Int
  type FooFType Int = []
  defPs = [3]
test @Bool @Int -- 1 or 3?

Interestingly enough, not even a type signature can save you here. It appears necessary to use a type application:

{-# LANGUAGE ExplicitForAll, ScopedTypeVariables, TypeApplications, ... #-}
test :: forall t. (Foo t, Foldable (FooFType t)) => FooPType t
test = head $ toList $ defPs @t

Upvotes: 1

Related Questions