Chapter 8 exercise "reverse" #111
Description
For reference, here's the template given in the material:
{-@ assume reverse :: xs:UList a -> UList a @-}
reverse :: [a] -> [a]
reverse = go []
where
{-@ go :: acc:[a] -> xs:[a] -> [a] @-}
go acc [] = acc
go acc (x:xs) = go (x:acc) xs
The empty list given to go has (vacuously) only unique values, hasn't it? I tried to bind it in a variable and declare it as unique as follows:
reverse :: [a] -> [a]
reverse = go seed
where
{-@ seed :: UList a @-}
seed = []
go acc [] = acc
go acc (x:xs) = go (x:acc) xs
This led into a weird error:
[ 9 of 13] Compiling Tutorial_08_Measure_Set
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.1:
Uh oh.
Predicate in lhs of constraint:forall <p :: a a -> Bool>.
{lq_tmp$x##7006 : [a]<\lq_tmp$x##7007 VV -> {lq_tmp$x##7005 : a<p lq_tmp$x##7007> | true}> | Tutorial_08_Measure_Set.elts lq_tmp$x##7006 == Set_empty 0
&& (Tutorial_08_Measure_Set.unique lq_tmp$x##7006 <=> true)
&& len lq_tmp$x##7006 == 0
&& Set_emp (listElts lq_tmp$x##7006)}
<:
{VV##0 : [a] | Tutorial_08_Measure_Set.unique VV##0}
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
I wonder what's the issue here.