Allow to import type and predicate aliases qualified

[facundominguez]

This is a spin off of #2169.

Liquid Haskell allows to express type and predicate aliases. For instance,

module Nat where
{-@ type INat = {v:Int | v >= 0} @-}


module Length where
import Nat

{-@ llength :: [a] -> INat @-}
llength :: [a] -> Int
llength [] = 0
llength (_:xs) = 1 + length xs

Unfortunately, aliases live in a flat namespace, which implies that if different modules define the same aliases, they will result in ambiguity.

module Nat1 where
{-@ type INat = {v:Int | v >= 0} @-}


module Nat2 where
import Data.Int (Int32)
{-@ type INat = {v:Int32 | v >= 0} @-}


module Length where
import Nat1
import Nat2

-- Nat is ambiguous in the following spec because it could be either
-- of 'Nat1.Nat' or 'Nat2.Nat'. If we try to qualify 'Nat', however,
-- we will get an error saying that the qualified name is not in scope.
{-@ llength :: [a] -> INat @-}
llength :: [a] -> Int
llength [] = 0
llength (_:xs) = 1 + length xs

Ideally, Liquid Haskell would honor the module aliases of import declarations. So in the above example, we can write instead

module Length where
import qualified Nat1 as N
import Nat2

{-@ llength :: [a] -> N.INat @-}
llength :: [a] -> Int
llength [] = 0
llength (_:xs) = 1 + length xs

Besides making name resolution of aliases consistent with the rest of the Liquid Haskell constructs, this would also fix #2446.

[f-ei8ht]

Hi @facundominguez,

I came across this issue while exploring Qualified Aliases in Liquid Haskell for GSoC 2025. I noticed that it has been open since February 4, 2025. Is there any specific direction or existing work related to this? I’d love to understand its scope and potential challenges before considering it for my GSoC proposal.

I am very interested in this project and have recently started learning Haskell. While I may not be highly experienced yet, I am committed to learning and contributing as much as possible. Even if I don’t get selected for GSoC, I intend to put in my best effort to contribute meaningfully.

Looking forward to your insights!

Best regards,
Saif Ali Khan

[facundominguez]

Hello @f-ei8ht, and welcome!

One way to approach LH could be by building it and then trying it on some examples that involve type and predicate aliases. After growing the sense of how to test the feature, one could move to explore how it is implemented.

The documentation of compiler plugins is a prerequisite to approach the code, as Liquid Haskell is implemented as a compiler plugin which has this entry point.

For the part of the implementation specific to this ticket, this is were name resolution is implemented.

Also, there is this blog post about name resolution in LH, and #2169 can provide some more details.

One useful check to decide if someone is ready for design is describing in some detail how the current implementation of name resolution works for aliases both when defined in the current module and when imported from elsewhere. I expect that a fair amount of reading the code will still be necessary.

From then on, I guess that a design discussion could be started :)

[f-ei8ht]

Thank you sir, this is a very solid approach, I’ll go through the compiler plugin documentation and the name resolution code as well.

I’ll also check out the blog post and #2169 for more context. Once I have a clear understanding of how things work, I’ll reach out!

Thank you, again.

[facundominguez]

One of the candidates to GSoC noted that predicate aliases are mentioned as deprecated in this section of the documentation, which brings up the question on whether they should be phased out instead of fixed in the same way as type aliases. I think it would be fine to analyze the matter as part of the project.