Reflected function on GADT needs explicit type annotation

[rosekunkel]

The following triggers an LH error:

{-# LANGUAGE GADTs #-}
{-@ LIQUID "--reflection" @-}

module Gadt where

data Foo a where
  Bar :: Foo Int
  Baz :: Foo Bool

{-@ reflect getFoo @-}
getFoo :: Foo a -> a
getFoo Bar = 123
getFoo Baz = True

The error is

Error: Illegal type specification for `Gadt.getFoo`

 11 | {-@ reflect getFoo @-}
                  ^^^^^^

     Gadt.getFoo :: forall a##xo .
                    lq1:(Gadt.Foo a##xo)
                    -> {VV : a##xo | VV == getFoo lq1}
     Sort Error in Refinement: {VV : a##aWl | (VV == Gadt.getFoo lq1
                                               && VV == (if is$Gadt.Bar lq1 then GHC.Num.fromInteger (coerce (GHC.Num.Num int) ~ (GHC.Num.Num a##aWl) in GHC.Num.$fNumInt) 123 else (coerce bool ~ a##aWl in true)))}
     Unbound symbol GHC.Num.fromInteger --- perhaps you meant: GHC.Types.IntRep, GHC.Enum.C:Bounded, GHC.Real.C:Integral ?

However, if we explicitly annotate the type of 123, it passes:

{-# LANGUAGE GADTs #-}
{-@ LIQUID "--reflection" @-}

module Gadt where

data Foo a where
  Bar :: Foo Int
  Baz :: Foo Bool

{-@ reflect getFoo @-}
getFoo :: Foo a -> a
getFoo Bar = 123 :: Int
getFoo Baz = True

[ranjitjhala]

Grr that’s a bit odd that GHC puts in the unnecessary “fromInteger” ...

Still would be nice to somehow use the typesig to generate a term to use in the reflected body... hmm.

On Thu, Mar 14, 2019 at 4:25 PM Rose Kunkel notifications@github.com wrote:

The following triggers an LH error:

{-# LANGUAGE GADTs #-} {-@ LIQUID "--reflection" @-} module Gadt where data Foo a where Bar :: Foo Int Baz :: Foo Bool

{-@ reflect getFoo @-}getFoo :: Foo a -> a getFoo Bar = 123 getFoo Baz = True

The error is

Error: Illegal type specification for Gadt.getFoo

11 | {-@ reflect getFoo @-} ^^^^^^

 Gadt.getFoo :: forall a##xo .
                lq1:(Gadt.Foo a##xo)
                -> {VV : a##xo | VV == getFoo lq1}
 Sort Error in Refinement: {VV : a##aWl | (VV == Gadt.getFoo lq1
                                           && VV == (if is$Gadt.Bar lq1 then GHC.Num.fromInteger (coerce (GHC.Num.Num int) ~ (GHC.Num.Num a##aWl) in GHC.Num.$fNumInt) 123 else (coerce bool ~ a##aWl in true)))}
 Unbound symbol GHC.Num.fromInteger --- perhaps you meant: GHC.Types.IntRep, GHC.Enum.C:Bounded, GHC.Real.C:Integral ?

However, if we explicitly annotate the type of 123, it passes:

{-# LANGUAGE GADTs #-} {-@ LIQUID "--reflection" @-} module Gadt where data Foo a where Bar :: Foo Int Baz :: Foo Bool

{-@ reflect getFoo @-}getFoo :: Foo a -> a getFoo Bar = 123 :: Int getFoo Baz = True

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1422, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOFQfluIe1iMBU9qR2_3ZveXo6KUBks5vWtpKgaJpZM4b1aGR .