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 ***@***.***> 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 <#1422>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOFQfluIe1iMBU9qR2_3ZveXo6KUBks5vWtpKgaJpZM4b1aGR> .