Type mismatch in signature and locally introduced term-CodePudding

Consider the following code:

-- | Parse a 64bit word in little-endian format.
word64le :: Get ByteString e Word64
word64le = do
    s <- elems 8
    pure $ foldl' (.|.) 0 [shiftL (fromIntegral b) (i * 8) | (i, b) <- zip [0 .. 7] (atomize s)]

Per the comment, this reads out a Word64 from a ByteString by first pulling an 8-byte ByteString (the elems call), then unpacking it (the atomize call) and doing the obvious shift left dance. So far so good. Now this code can very obviously be generalized to other machine integral types, we just need to get hold of the number of bits of such a type and that is supplied by the FiniteBits class. So doing the generalization:

-- | Parse an integral word in little-endian format.
integralLe :: (FiniteBits w, Integral w, Bounded w) => Get ByteString e w
integralLe = do
        s <- elems (fromIntegral n)
        pure $ foldl' (.|.) 0 [shiftL (fromIntegral b) (i * 8) | (i, b) <- zip [0 .. n - 1] (atomize s)]
    where
        n = finiteBitSize (minBound :: w) `quot` 8

This does not work, with GHC complaining that "Could not deduce (Bounded w1) arising from a use of ‘minBound’ from the context: (FiniteBits w, Integral w, Bounded w)". So it seems that my type annotation minBound :: w is not enough to convince GHC that I mean the same w as in the function signature; is my diagnosis correct? And if yes, how do I tell GHC that the two w types are the same?

note(s):

on GHC 9.2 with a nightly stackage.
sorry about the poor question title, but cannot think of anything better.

edit(s):

per the comment added {-# LANGUAGE ScopedTypeVariables #-} at the top of the file but having the same error, namely "Could not deduce (Bounded w2) arising from a use of ‘minBound’ from the context: (FiniteBits w, Integral w, Bounded w) bound by the type signature for:"
Aha. If I add an explicit forall e w . in the function signature to the left of the constraint it works, even without the ScopedTypedVariables extensions (maybe because I am using language GHC2021). No on, to understand why the heck this works...

CodePudding user response：

Haskell has some... let's charitably call it "weird"... rules for how type variables are scoped by default.

-- | Parse an integral word in little-endian format.
integralLe :: (FiniteBits w, Integral w, Bounded w) => Get ByteString e w
integralLe = do
        s <- elems (fromIntegral n)
        pure $ foldl' (.|.) 0 [shiftL (fromIntegral b) (i * 8) | (i, b) <- zip [0 .. n - 1] (atomize s)]
    where
        n = finiteBitSize (minBound :: w) `quot` 8

You're right that Haskell will throw an implicit forall w at the start of the integralLe type signature, but it's not actually a ScopedTypeVariables forall. By default, the scope of that variable is just that one line. It is not considered a type variable inside of any type ascriptions or signatures in where clauses, let clauses, or anything else inside the function. That's where ScopedTypeVariables comes in. With ScopedTypeVariables, an explicit forall makes the type variable available lexically to anything inside of the function body, including where blocks. (And, as you've correctly noted, ScopedTypeVariables is included in GHC2021). Hence,

integralLe :: forall w. (FiniteBits w, Integral w, Bounded w) => Get ByteString e w

will work.