Why doesn't the below type-check? The type of _
is inferred as Double.
{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}
module Main (main) where
data D a = D a
main =
let
n = D (1 :: forall a. (Floating a) => a)
in
case n of
D (_ :: forall a. (Floating a) => a) -> return ()
It appears that the type you are expecting for
n
isD (forall a. (Floating a) => a)
, but that is emphatically not the type that is inferred. In fact, if you try and add that type annotation ton
, you will find that GHC will loudly complain. Such a type would require GHC to support impredicative polymorphism, and it currently does not (for more information on what that is and why it is complicated, see What is predicativity?).The type that is actually inferred for
n
isD Double
. This is actually the result of two things at play: the dreaded monomorphism restriction and Haskell’s type defaulting rules. Due to the monomorphism restriction,n
must be inferred to be a monomorphic type (since it is not syntactically a function and does not have an explicit type annotation). For this reason,D 1
would be ambiguous, since1 :: forall a. (Floating a) => a
is polymorphic. However, in this case, Haskell has defaulting rules for numeric types, mostly to avoid the need to resolve ambiguities due to Haskell’s polymorphic number literals.Since you have explicitly added a type annotation to
1
to make itFloating
, then Haskell applies its default rule for floating-point types and defaults toDouble
. Therefore, the type ofn
is inferred to beD Double
.If you disable the monomorphism restriction, then the type of
n
would be the slightly more interesting typeforall a. Floating a => D a
, but that is the simpler universally quantified type rather than the existentially quantified one that you want.