You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
module Arity where
{-@ data T a <p :: a -> Prop, q :: a -> Prop > = MkT (t_x :: a) @-}
data T a = MkT a
-- error spec 1
{- f :: forall <p :: a -> Prop, q :: a -> Prop>. T <p> a -> a @-}
-- error spec 2
{- f :: forall <p :: a -> Prop, q :: a -> Prop>. T <p, q, {\ y -> (true)}> a -> a @-}
f :: T a -> a
f (MkT x) = x
The first spec, if used, produces:
LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.
liquid:
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
safeZipWith called on non-eq-sized lists (nxs = 2, nys = 1) : appRefts: Arity.T
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
This at least contains enough information to figure out it's a misapplication of Arity.T, but requires manually inspecting everywhere you wrote a LH spec using T.
The second spec's error is less helpful:
LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.
liquid:
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
YUCKER
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
This one also requires looking at all uses of T in LH specs, but I figured this out purely by luck. Curiously, if you replace the lambda in that spec with another use of p or q, the file type-checks despite the bad type application.
The text was updated successfully, but these errors were encountered:
The first spec, if used, produces:
This at least contains enough information to figure out it's a misapplication of Arity.T, but requires manually inspecting everywhere you wrote a LH spec using T.
The second spec's error is less helpful:
This one also requires looking at all uses of T in LH specs, but I figured this out purely by luck. Curiously, if you replace the lambda in that spec with another use of p or q, the file type-checks despite the bad type application.
The text was updated successfully, but these errors were encountered: