liquidhaskell
liquidhaskell copied to clipboard
"Specified type does not refine Haskell type" when using type classes
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,
- The type class instance
Data.Foldable.Foldable t
gets placed before the universalsforall b a
and - The type variables
a
andb
get incorrectly substituted byt
.
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 @-}