liquidhaskell icon indicating copy to clipboard operation
liquidhaskell copied to clipboard

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

Open pacastega opened this issue 5 months ago • 0 comments

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 @-}

pacastega avatar Sep 19 '24 11:09 pacastega