`autosize` fails on abstractly-refined, instance-deriving data

[awstlaur]

{-@ autosize List @-}

{-@ data List a <p :: a -> Prop>
      = N | C {hd :: a<p>, tl :: List a}
  @-}
data List a = N | C a (List a)
    deriving (Eq)

**** RESULT: ERROR *************************************************************

 <no location info>: Error: Uh oh.
     Constraint.instanctiatePv

If we remove the deriving (Eq) part, or if we remove the abstract refinement (below), then there is no error.

{-@ autosize List @-}

{-@ data List a
      = N | C {hd :: a, tl :: (List a)}
  @-}
data List a = N | C a (List a)
    deriving (Eq)

**** RESULT: SAFE **************************************************************

[nikivazou]

Thanks!

Does the easy work around work? To define the Eq instance yourself (for now).

[awstlaur]

Yes that will definitely work. (In fact, I probably won't even be using autosize after all; I was mostly curious and then stumbled into this.)

[ranjitjhala]

Thanks for pointing this out!