Type annotation breaks function

Question

Consider the following declarations for a function f' using singletons with the Frames library (which defines UnColumn and AllAre), and a wrapper function using withSing.

{-# LANGUAGE AllowAmbiguousTypes -#}
import Frames
import Data.Singletons.Prelude

f' ::  forall rs1 rs2 a. (AllAre a (UnColumn rs1), AllAre a (UnColumn rs2), Num a)
      => SList rs1 -> SList rs2 -> Frame (Record rs1) -> Frame (Record rs2) -> Int
f' = undefined

f df1 df2 = withSing (withSing f') df1 df2

This seems to work fine. But when I add a type annotation, type checking fails with the error Could not deduce: (AllAre a0 (UnColumn rs1), AllAre a0 (UnColumn rs2)).

f :: (SingI rs1, SingI rs2, AllAre a (UnColumn rs2), AllAre a (UnColumn rs1), Num a)
=> Frame (Record rs1) -> Frame (Record rs2) -> Int
f df1 df2 = withSing (withSing f') df1 df2

The thing is, this is precisely the inferred type signature, according to GHCi (well, Intero). To my understanding adding an explicit signature matching the inferred signature should have no impact on the code semantics, so why would this break the code?

Answer 1

As a general rule of thumb, adding an explicit type signature that matches the inferred type to a Haskell program will not change its meaning, but it's not actually guaranteed in the general case. (I believe it is guaranteed for top-level definitions in Haskell98, though.)

Ultimately, your problem isn't much different from the sort of type variable scoping problem that can happen with local definitions in Haskell98:

import Data.List
sortImage :: Ord b => (a -> b) -> [a] -> [a]
sortImage f = sortBy cmp
  where cmp x y = compare (f x) (f y)

Here, the inferred type of cmp is effectively (Ord b) => a -> a -> Ordering. You can't make this signature explicit, though, because you can't tie a and b back to the outer signature (and the type of f in particular) unless you use ScopedTypeVariables, in which case you can write:

sortImage :: forall a b . Ord b => (a -> b) -> [a] -> [a]
sortImage f = sortBy cmp
  where cmp :: a -> a -> Ordering
        cmp x y = compare (f x) (f y)

As you've discovered, you can make this sort of type variable scoping problem happen with top level definitions, too, at least with AllowAmbiguousTypes enabled.

Here is a simpler example that illustrates what I believe is the same problem, adapted from the GHC documentation on the AllowAmbiguousTypes extension:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

class D a b
instance D Bool b
instance D Int b

strange :: D a b => a -> a
strange = undefined

-- stranger :: (D a b1, D a b) => a -> a
stranger x = strange (strange x)

I've shown the inferred type of stranger as a comment. If you try to make it explicit, you'll get the error:

• Could not deduce (D a b0) arising from a use of ‘strange’ from the context: (D a b2, D a b)

The issue is that GHC can infer that stranger can be called on any a that satisfies D a b1 for the outer strange :: D a b1 => a -> a and also satisfies D a b for the inner strange :: D a b => a -> a.

However, if you attempt to make this type signature explicit, the link between the b1 and b variables in the explicit signature for stranger and their relationship to the types of the strange calls is lost, much as the relationship between the a and b in a hypothetical cmp signature and the a and b in the sortImage signature is lost in the first example.

Using ScopedTypeVariables alone isn't enough to solve the problem here because, constraints aside, the type of strange is just a -> a and doesn't directly reference b. So, you can write:

stranger :: forall a b1 b2 . (D a b1, D a b2) => a -> a
stranger x = (strange :: a -> a) ((strange :: a -> a) x)

but you can't tie the b1 and b2 to the types of the strange calls. You need TypeApplications to do that:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

class D a b
instance D Bool b

strange :: forall a b . D a b => a -> a
strange = id

stranger :: forall a b1 b2 . (D a b1, D a b2) => a -> a
stranger x = (strange @a @b1) (strange @a @b2 x)

and then it type checks okay, and you can even call:

> stranger False
False

without any type annotations (which is somewhat surprising). If you had an instance:

instance D Int Double

though, then you'd need to be explicit to use stranger on Ints:

> stranger @_ @Double @Double (1 :: Int)