ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

"Specified type does not refine Haskell type" when using type classes #2341

Open pacastega opened 2 months ago

pacastega commented 2 months ago

When trying to assume the type of a Haskell function involving type classes:

module Fold where
{-@ assume foldl :: (b -> a -> b) -> b -> t a -> b @-}

Liquid Haskell gives the following error:

    Specified type does not refine Haskell type for `Data.Foldable.foldl` (Checked)
The Liquid type
.
    forall t ->
Data.Foldable.Foldable t
-> forall b a -> (t -> t -> t) -> t -> t t -> t
.
is inconsistent with the Haskell type
.
    forall (t :: GHC.Types.Type -> GHC.Types.Type) b a.
Data.Foldable.Foldable t =>
(b -> a -> b) -> b -> t a -> b
.
defined at UnhelpfulNoLocationInfo
.
  |
3 | {-@ assume foldl :: (b -> a -> b) -> b -> t a -> b @-}
  |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

That is,

  1. The type class instance Data.Foldable.Foldable t gets placed before the universals forall b a and
  2. The type variables a and b get incorrectly substituted by t.

This also happens when writing the existentials and type classes explicitly:

{-@ assume foldl :: forall t b a .
                    Foldable t => (b -> a -> b) -> b -> t a -> b @-}