GHC Type Inference - Too clever for its own good?

Learn
#1

Sometimes GHC is far too smart (for me).

Two functions (from here).

f :: (RealFloat a) => Maybe (Complex a) -> Maybe (Complex a) -> Maybe (Complex a) -> Maybe (Complex a)
f m1 m2 r = g ⊗ m1 ⊗ m2 ⊘ sq r
  where
    g = to 6.67 ⊗ (to 10 ⊗⊗ negate' (to 11))

f' :: (RealFloat a, Num (Maybe (Complex a))) => Maybe (Complex a) -> Maybe (Complex a) -> Maybe (Complex a) -> Maybe (Complex a)
f' m1 m2 r = g ⊗ m1 ⊗ m2 ⊘ sq r
  where
    g = to 6.67 ⊗ (to 10 ⊗⊗ negate' 11)

The difference is in how the negate' function is called.

to :: (Num a) => a -> Maybe (Complex a)
to a = Just $ a :+ 0

negate' :: (RealFloat a) => Maybe (Complex a) -> Maybe (Complex a)
negate' = fmap negate

The f' negate call is clearly wrong, and yet somehow GHC infers a typeclass constraint which on some level must type check.

Of course when I try to execute f' it fails because it cannot find the instance it inferred…

These type of failures are always curiosities to me. The naive solution seems easiest to find and more correct…

How should I think about this? Maybe I just misunderstand the f' function…

In future I think I’ll just provide explicit type definitions, might make things clearer…

1 Like
#2

Before you go adding type signatures everywhere - remember that the partially-applied function type ((->) a) also has it’s own Functor instance: this (along with its Applicative and Monad instances) has contributed to some confusion in the past…

2 Likes
#3

This is usual behaviour for any inferred instance – even for Eq or Show. GHC (and Haskell in general) features separate compilation to support modular decomposition of a program. In particular to support a comprehensive library infrastructure. (I’m old enough to remember ‘monolithic programming’ where you might include ‘copy modules’ of program code pasted in from a library, but no guarantee that code was valid/well-typed. Good luck with several hundred pages of expanded text figuring out what was causing the compile fail.)

So when compiling this module, GHC doesn’t know what other modules it’s going to be combined with, and that’ll supply further instances.

Is it? Clearly? You’ve given a signature for f' (good discipline); the code including the negate' call type-checks against it. (So it’s misleading to say “infers a typeclass constraint”. Yes GHC infers a constraint from the code; it then checks it against the given signature; the inferred constraint is not more restrictive than the given.) Then it’s right. Perhaps you could have given a more specific signature? Then it’s the signature that’s wrong.

1 Like
#4

Well, I would prefer that your favourite IDE would just show you the inferred type in e.g. a small “floating text-box”, by right-clicking on the function’s definition (or just letting the mouse sit on the function’s name) - rewriting a whole “cascade” of type signatures just to use e.g. some “new-fangled” monadic-transformer effect deep inside a program is such a boring chore…

#5

What I mean by that is (I hope) you’ve thought in advance about how to break down the overall application into manageable chunks (functions); and thought how they’re going to interact by giving each an interface – that is, a signature. If on the other hand:

that’s what I would describe as ‘cargo cult programming’: " copies some program code from one place to another" (that is, copies signatures from the IDE-inferred (or compiler-inferred) type into your code without passing through your brain.) It would be more honest to not give a signature [**] in that case, to show readers of your code how much understanding hasn’t gone into it.

I assumed @mmport80’s question is coming from a relative newbie, not wrt a monadic-transformer wotsit. Then yes it adds to a learner’s learning to see what types get inferred; but it’s a terrible habit to get in to. And means when a newbie sees a GHC type-error message they treat it as gospel, again without real understanding. Whoever’s responsible for GHC’s message To defer the ambiguity check to use sites, enable AllowAmbiguousTypes should be publicly flogged on a regular basis; and indeed the design that AllowAmbiguousTypes is a module-wide setting, not specific to the usage site should also get publicly harangued.

[**] Haskell’s type system used to be (and still largely is derived from) Hindley-Damas-Milner, which needs no type annotations in bread-and-butter code.

1 Like
#6

your favourite IDE would just show you the inferred type by right-clicking on the function’s definition

that’s what I would describe as ‘cargo cult programming’: “copies some program code from one place to another” (that is, copies signatures from the IDE-inferred (or compiler-inferred) type into your code without passing through your brain.)

My intention was to avoid having type signatures everywhere in code, in the same way we don’t always have to provide the correct order of evaluation:

Both of these are annoying relics of older programming languages that now usually only interest speed enthusiasts.

But you have a valid point - it would also make it easier to just “copy-n-paste” inferred types into type signatures, for those who really do want those signatures everywhere… :-/

#7

Yes, I’m all for avoiding that sort of clutter: signatures at the top level of a module; or for complex functions with non-obvious manipulations (to help the reader and the compiler ‘keep you honest’); and where you want to restrict the type to be less general than inferred. Otherwise not.

I guess we should wait for o.p.'s feedback as to why they want this signature/was f''s signature deliberate/was it the result of careful thought/was it just pasted from what the compiler offered?

But why would you want a signature everywhere? What value is it adding if it’s merely what the compiler infers anyway?

1 Like
#8

No - not any one signature everywhere, just the proliferation/over-use of them in general. But I agree that this is tangentially-related (at best) to the original topic…

1 Like
#9

It was just copied from HLS - as part of understanding how it could typecheck : )

#10

Okaaay … Then some learnings:

  1. Don’t do that. (That is, by all means use HLS to see GHC’s guess at the inferred type. Don’t just paste that dumbly in to your code.)
  2. The more ugly and convoluted your expression, the more important to write the type sig first – as a sanity check.
  3. If you think two functions should have the same type, give them the same type sig. If it turns out GHC (or HLS) disagree, you might end up seeing they are different. But treat those tools as your servant, not your friend, and certainly not your instructor.
  4. Specifically wrt Haskell’s numeric hierarchy, Prelude.negate :: Num a => ...; negate' :: (RealFloat a) => ..., so it’s requiring the a be more specific. f :: (RealFloat a) => ... so that’s just as specific. f' :: (RealFloat a, Num (...)) => .... So the RealFloat a is equally specific … except Huh? Something less specific than RealFloat? And there’s an a embedded in there.

Then the alarm bell should have sounded when firstly HLS gave you two numeric-ish constraints both constraining a, secondly when one was Num rather than RealFloat.

#11

Yeh… You know, in my experience going off-piste is when type inference stops working…

And in this case, as you say, the inference is misleading even when I really don’t think the function is all that difficult…

I suppose there’s just a learning curve to inference, and I hit a small kink : ) I suppose it’s doing so well, that when I hit a few bumps, I’m unsure what to do.

Thanks again for your help. I will definitely start manually writing definitions!

#12

I think you have a point in that type inference and type class overloading may sometimes yield surprising results.

But in your case I fail to even understand the example. Is this really the most minimal example you could come up with?

Furthermore, I don’t see “The f' negate call”. There are no calls to f' whatsoever.
You somehow seem to dislike the type signature for f', yet you seem to be OK with the one for f. Is that right?

Often what is most confusing to me is not that GHC is able to infer the most general type. It is often that the most general type is not what I expect it to be!

Just recently I had something like

import qualified Data.List.NonEmpty as NE

data T = Many (NE.NonEmpty T)
       | Leaf Int

count :: NE.NonEmpty T -> Int
count ts = length $ reassoc ts
  where
    reassoc ts = concatMap one ts
    one (Many (t NE.:| ts)) = one t <> reassoc ts
    one t = pure t

This program will error on length $ reassoc ts, saying that ts has not expected type [T]:

test.hs:14:29: error:
    • Couldn't match expected type: [T]
                  with actual type: NE.NonEmpty T
    • In the first argument of ‘reassoc’, namely ‘ts’
      In the second argument of ‘($)’, namely ‘reassoc ts’
      In the expression: length $ reassoc ts
   |
14 | count ts = length $ reassoc ts
   |                             ^^

But this is very confusing, because the error is actually with the definition of one, which calls reassoc with a [T] instead of the expected NonEmpty T! I.e.,

count :: NE.NonEmpty T -> Int
count ts = length $ reassoc ts
  where
    reassoc ts = concatMap one ts
    one (Many (t NE.:| ts)) = case NE.nonEmpty ts of
      Nothing  -> one t
      Just ts' -> reassoc ts'
    one t = pure t

would be the correct code in my case.

Note that the “wrong” code type-checked with a most general type that was incompatible with the type expected at the use site, leading to a type error at a location that I did not expect.
It is very hard for the compiler to do a better job here; after all, the “wrong” definition of one type-checks.
I would have easily caught this error early if I was required to give a type signature for one/reassoc.

#13

So apparently it was the composition of sub-expressions (and their types) which was the problem there:

https://gergo.erdi.hu/projects/tandoori/

I would have easily caught this error early if I was required to give a type signature for one/reassoc.

…and people could probably stop space leaks from occurring if only they had direct access to (the “equivalents” of) malloc and free.

What stops people from making mistakes when adding type signatures? It’s just more source code…

#14

Of course there would be minimal examples showing GHC infers a too-general type. But they would be easy to spot. The point here is that mmport80’s f''s RHS is a convoluted expression with many operator and function applications. Not at all easy to see what the type should be. Not easy to see that GHC’s inferred type is wrong. Hence my ‘Don’t do that’.

I don’t know how long you’ve been programming, or in which languages: this is normal. It’s especially normal with Haskell’s type inference being so darn smart (by which I mean stupid). It’s normal for a problem with a definition/declaration not to show up until a usage site. If you get a weird type-error rejection, the first thing to do is check your definitions. (This is why I hate AllowAmbiguousTypes so vehemently: it’s more-or-less saying ‘please GHC make me as confused as possible by shunting all the validation to the place it’s going to be hardest to understand’.)

Excellent reason for the discipline of writing the type sig before writing the function body.

Nothing we’ve said in the earlier discussion is against giving sigs within a where. In particular, ever since the FTP brouhaha, things like concatMap have such a vague type, they should come with a health warning.

If you’re not confident you can predict the types reading your own code, nobody else reading the code will be able to either. Give a sig.

#15

Sometimes I think we should make a more principled distinction between abstraction and overloading. In Haskell we use typeclasses for both, but there is a clear difference between the two use-cases. If we use a typeclass method for writing abstract code then we want type inference to generalize the definition and generate a typeclass constraint on the function signature. If we use a typeclass method for overloading then we never want the typeclass constraint to appear in a type signature, because we always want to statically know to which instance the method resolves.

Two examples of typeclasse constraints which I never want to see in type signatures are Default a and HasField x r a. If type inference cannot resolve which concrete instance my def or getField refers to, then I would prefer it to emit an error instead of generalizing the constraint.

2 Likes
#16

I agree in principle, but would you say that foldr/concatMap is abstracted or overloaded? I find it hard to draw a line.

Perhaps it would help if all type class method calls required explicit type args if the constraint cannot be immediately discharged with a Given. E.g., foldr (+) 0 [1,2,3] :: [Int] is fine, whereas mySum = foldr (+) (0::Int) is not, because it would have an ungeneralised Foldable f constraint. You would be allowed to write mySum @f = foldr @f (+) (0::Int), though, signifying that you are well aware that the caller might have to supply some dictionaries for f as well. Opt-in overloading, so to speak. Of course this doesn’t really work for nullary constraints such as Partial, but there it’s good to give a full type signature anyway.