From 2dd6c1027c62cfaa1a445452affb96375c4a728d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 10 Jul 2024 07:36:40 +0200
Subject: [PATCH] fix(hax-lib): `use super::*` in refinement expansion

This commit fixes #761.

Considering:
```rust
use some::path::to::T;

pub struct MyRefinedType(T);
```

The generated code wraps the struct declaration in a module.
That module used not to have `T` in scope.

This commit adds a `use super::*` before declaring the type of the
refinement type.
---
 hax-lib-macros/src/lib.rs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 30b1b7ff7..2a237dd47 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -820,6 +820,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
     quote! {
         #[allow(non_snake_case)]
         mod #module_ident {
+            #[allow(unused_imports)]
+            use super::*;
+
             #refinement_item
 
             #newtype_as_ref_attr
@@ -828,7 +831,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
 
             #[::hax_lib::exclude]
             impl #generics ::hax_lib::Refinement for #ident <#generics_args> {
+
                 type InnerType = #inner_ty;
+
                 fn new(x: Self::InnerType) -> Self {
                     #debug_assert
                     Self(x)