Element refinement is not inferred for indexed container

[gergoerdi]

The following module demonstrates creating an un-indexed container List and a (Nat-)indexed container Vec, where refining the element type works for everything up to the definition of ys1. That is, the following module on its own typechecks:

import Prelude (Bool(..))
import GHC.TypeLits

data List a = LCons a (List a) | LNil

{-@ type T = {b : Bool | b} @-}

{-@ xs0 :: List T @-}
xs0 :: List Bool
xs0 = LNil

{-@ xs1 :: List T @-}
xs1 :: List Bool
xs1 = LCons True LNil

data Vec (n :: Nat) a where
    VCons :: a -> Vec n a -> Vec (1 + n) a
    VNil :: Vec 0 a

type Vec0 = Vec 0 -- Workaround for https://github.com/ucsd-progsys/liquidhaskell/issues/2080
{-@ ys0 :: Vec0 T @-}
ys0 :: Vec0 Bool
ys0 = VNil

But if I add the following definition to it as well, then it doesn't pass the LH typechecker:

type Vec1 = Vec 1 -- Workaround for https://github.com/ucsd-progsys/liquidhaskell/issues/2080
{-@ ys1 :: Vec1 T @-}
ys1 :: Vec1 Bool
ys1 = VCons True VNil

error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : GHC.Types.Bool
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Bool | VV}
    .
    Constraint id 24
   |
31 | ys1 = VCons True VNil
   | ^^^

[nikivazou]

The following passes:

{-@ vCons :: a -> Vec0 a -> Vec1 a @-}
vCons :: a -> Vec0 a -> Vec1 a 
vCons = VCons 

type Vec1 = Vec 1 -- Workaround for https://github.com/ucsd-progsys/liquidhaskell/issues/2080
{-@ ys1 :: Vec1 T @-}
ys1 :: Vec1 Bool
ys1 = vCons True VNil

The reason why type checking should go through is that the type variable a gets instantiated with the refined T. I assume (I have to check the core to be sure and hopefully fix it...) that the (n :: Nat) constrain in the definition of Vec makes LH think that the a type variable is also constraint and does not permit instantiation with refined types... In my vCons definition a is clearly not constraint.

[nikivazou]

BTW, the following also passes:

data Vec a (n :: Nat) where
    VCons :: a -> Vec a n -> Vec a (1 + n)
    VNil :: Vec a 0

{-@ ys1 :: Vec T _ @-}
ys1 :: Vec Bool 1
ys1 = vCons True ys0

{-@ vCons :: a -> Vec a _ -> Vec a _ @-}
vCons :: a -> Vec a 0 -> Vec a 1 
vCons = VCons

{-@ ys0 :: Vec T _ @-}
ys0 :: Vec Bool 0
ys0 = VNil

I guess, 1+n is internally, by ghc, encoded as a different type argument and the ordering LH violates some GHC assumption about the ordering of implicit arguments... Will try to take a deeper look soon...

[gergoerdi]

I guess, 1+n is internally, by ghc, encoded as a different type argument and the ordering LH violates some GHC assumption about the ordering of implicit arguments... Will try to take a deeper look soon...

The Core representation of that should be something like VCons :: forall a n m. (m ~ (1 + n)) => Vec a n -> Vec a m

[gergoerdi]

Oh, sorry, you probably meant the type of vCons the function, not VCons the constructor. So just to highlight it, given the following definitions (I moved from 1 + n to n + 1 just because that's how Clash defines vectors and that's what I'll want to use eventually):

{-@ type T = {b : Bool | b} @-}

data Vec :: Nat -> Type -> Type where
    VCons :: a -> Vec n a -> Vec (n + 1) a
    VNil :: Vec 0 a

{-@ ys1 :: Vec _ T @-}
ys1 :: Vec 1 Bool
ys1 = vCons True VNil

we can add this to complete it in a way that LH accepts:

{-@ vCons :: a -> Vec _ a -> Vec _ a @-}
vCons :: a -> Vec 0 a -> Vec 1 a
vCons = VCons

but this gets rejected by LH:

{-@ vCons :: a -> Vec _ a -> Vec _ a @-}
vCons :: a -> Vec n a -> Vec (n + 1) a
vCons = VCons

[gergoerdi]

also, this definition, on its own, is accepted by LH:

{-@ vCons :: a -> Vec _ a -> Vec _ a @-}
vCons :: a -> Vec n a -> Vec (n + 1) a
vCons = VCons

it just can't be used in the definition of ys1.

[nikivazou]

I actually meant the VCons the constructor. I assume this implicit GHC generated variable m confuses type abstraction of Liquid Haskell...