More complete RankNTypes support by JacobGH2 · Pull Request #494 · BillHallahan/G2

JacobGH2 · 2026-05-13T00:43:33Z

Changes (can point to place in code if more information is needed)

symbolic polymorphic function rules
--no-duplicate-outputs option
Validation doesn't stop at the first validation error. Distinguishes between source and validation (wrong output) errors.
other minor changes to Haskell printing
generating ADTs
Haskell printing of "generated" type class instances for validation
rewrites required for definitions involving typeclass dicts
test cases
misc. changes to support others
If initial expression has kind polymorphism, apply at @type, not @integer (what was done before)

If we want to split these up, I could remove the changes to validation (including the duplicate outputs option).

… infinite dupl. definitions

…plied type lambda arguments in result definitions

…ing type variable applications

…inor optimizations needed in FUN-ARG. FUN-ARG not general.

…retty print.

…ypes. PM-INST-ADT works for mixed concrete and polymorphic DataCon type arguments.

…rom an outer forall.

…same function for argument expressions.

…tion. Logging in ValidateState.

…s use 'deriving instance Eq'

…or all kind vars. Inputs are also made with kind vars subst'd.

…me issue when validating.

… cause mismatches. Some unneeded ADTs being printed (polyFuncArgTwoKinds)

…te outputs.

…eport to user. Some issues

…ch that handles gen instances

… outputs

BillHallahan · 2026-05-17T01:21:58Z


 -- | Solve for concrete values in a fully executed state.
-type SolveStates m r t = State t -> Bindings -> m (Result (r, NameGen) () ())
+type SolveStates m r t = State t -> Bindings -> m (Result (r, NameGen, Bindings) () ())


The Bindings have a NameGen in them- so would be better to just make this (r, Bindings).

BillHallahan · 2026-05-17T01:22:31Z

                   -> Bindings
                   -> State t
-                   -> IO (Result (ExecRes t, NameGen) () ())
+                   -> IO (Result (ExecRes t, NameGen, Bindings) () ())


Bindings contain a NameGen

BillHallahan · 2026-05-17T01:30:22Z

-                runToEnvText :: [(Name, Name)] -> T.Text
-                runToEnvText = T.intercalate "\n" . map (\(rTv, eTv) -> 
-                    mkNameHaskell pg rTv <> " -> " <> mkNameHaskell pg eTv)
+        prettyTyConcOrSym (TV.TySym (Id _ ty)) = "symbolic " <> mkTypeHaskell ty


Why this change? I think the Id indicates the TyVar Id?

I think this was left in from when I was trying to do symbolic types. Will remove.

BillHallahan · 2026-05-17T01:30:52Z

 solveStates' :: ( Named t
                , ASTContainer t Expr
-                , ASTContainer t G2.Type) => Bindings -> [State t] -> IO (Maybe (ExecRes t, NameGen))
+                , ASTContainer t G2.Type) => Bindings -> [State t] -> IO (Maybe (ExecRes t, NameGen, Bindings))


Binding has NameGen in it

BillHallahan · 2026-05-18T02:32:48Z

+filterToGenADTs :: TypeEnv -> TypeEnv
+filterToGenADTs = filterTE ((== ADTG2Generated) . adt_source)
+
+isEmpty :: TypeEnv -> Bool


Don't think we're using this anywhere? Cut.

BillHallahan · 2026-05-18T02:40:05Z

            frstck = S.pop stck

+-- | Separate a type into what is required for some RankNTypes rules.
+sepTypeForRNT :: Type -> ([Type], [Type], Maybe Type)


Comment, what is each of these lists/what is the Maybe?

BillHallahan · 2026-05-18T02:41:26Z

+                in (t1:ts', rest)
+        getTs mt = ([], mt) -- ignore last in tms, return as tr
+
+mkNestedLam :: LamUse -> [Id] -> Expr -> Expr


See
https://github.com/BillHallahan/G2/blob/master/src/G2/Language/Expr.hs#L407
Instead of this, just have mkLams (zip (repeat lu) vs) e?

BillHallahan · 2026-05-18T02:43:08Z

+mkNestedLam :: LamUse -> [Id] -> Expr -> Expr
+mkNestedLam lu vs e = foldr (Lam lu) e vs
+
+mkNestedForAll :: [Type] -> Type -> Type


Could we just make the type of this [Id] -> Type -> Type and avoid the possibility of an error?

Also, consider defining in G2.Language.Typing

BillHallahan · 2026-05-18T02:45:37Z

+
+        -- PM-INST-VAR
+        pmInstVar ng_in
+            | tr `elem` ts -- return type in arguments


Only do this if tr is TyVar? (Seems like it'd avoid some duplication with PM-RET-DC?)

BillHallahan · 2026-05-18T02:50:00Z

+
+        -- Do tyVar substitution in all StateDiffs. Needed 
+        -- when tracking generated type class instances.
+        alt_res'' = tyVarSubst tvnv alt_res'


Can't do this, sorry- instantiating type variables eagerly can cause problems for other systems (mostly having to do with GADTs.)

If you need to replace a single type variable that you know about and are instantiating to a specific type, that might be ok. I don't fully understand the problem being solved here.

Would probably also be fine to do tyVarSubst specifically on the TCInstDiff

JacobGH2 added 30 commits May 12, 2026 19:20

removed PolyArgMap functionality/references

f433312

PM-INST-VAR handles arb a1..an (creates nested type lambda)

4602cbf

PM-INST-VAR should handle arb a1..an and Tm

15171b2

PM-CYCLE work: fs type incorrect in eenv after, probably ForAll type.…

7d66f99

… infinite dupl. definitions

PM-NONCONT: working

9285de0

same TV name for forall and type lambda

ec08cc7

refactor repeated bindings in evalForAll

728e126

PM-UNWRAP working on different ADTs, issue among all rules with un-ap…

92a9d6c

…plied type lambda arguments in result definitions

PM-INST-ADT working, inefficient. errors in validating, probably miss…

d711068

…ing type variable applications

no more infinite cycling when only have type variable arguments

4b9199c

fresh type variable Ids in types of new symbolic functions for all rules

f656c21

func-arg added, untested

a5acd13

f type in FUN-ARG has correct return type, fixed typing/app issues. M…

652c085

…inor optimizations needed in FUN-ARG. FUN-ARG not general.

Applying TyVars to DataCon in PM-INST-ADT. TyVars showing in result p…

93159f6

…retty print.

Applying TyVars as Type expressions, not Ids

f939b85

PM-CONST rule. Guard in PM-INST-ADT to force PM-CONST.

fe3253f

dataConTypeArgs finds types correctly for currently handled DataCon t…

7929ff0

…ypes. PM-INST-ADT works for mixed concrete and polymorphic DataCon type arguments.

Immediately cycle function argument in FUN-ARG

2d9b3d0

New tests

37a8dc1

Use ts from unTyApp result as type arguments to DCs in PM-INST-ADT

8d3b592

Parentheses around foralls in pretty printing.

c3ab523

Wrong expression inserted in eenv when removing PolyArgMap references

53daf0b

SF-FUNC-FORALL: working for specific types. Not retyping all needed TVs.

5c6e01b

SF-FUNC-FORALL: Handle functions with any number of a's.

387187c

Tests for Rank3 and greater

48055c2

Refactor RankN tests

45e77b4

PM-FUN-FORALL: Handle polymorphic funcion arguments which use types f…

cf9f436

…rom an outer forall.

Refactor manual Namegen passing to foldr

21dac73

Reworked foldr and rule logging.

c9b62f9

Direct symbolic arguments in PM-FUNC. PM-FUNC and PM-FUNC-FORALL use …

4c44924

…same function for argument expressions.

JacobGH2 added 28 commits May 12, 2026 19:20

Problem test cases (not in test suite yet).

a23ab6e

pretty printing fix that allows function kinds to validate

871cf87

Attempt at generating higher kinded types recursively. Failing valida…

f01c63c

…tion. Logging in ValidateState.

Changes to creating data declarations for validation. All declaration…

ce8f572

…s use 'deriving instance Eq'

When main expression is a kind-polymorphic function, apply at @type f…

878d47d

…or all kind vars. Inputs are also made with kind vars subst'd.

Gen adts in PM-FUNC-FORALL. forallWithPolyFuncArg2 causing gen adt na…

9ced0f5

…me issue when validating.

working with some mismatches

c5c9498

Print gen ADTs referenced by those in arguments.

be0a667

Print recurs. reachable generated ADTs. Don't add Names from ADT that…

1ffaeea

… cause mismatches. Some unneeded ADTs being printed (polyFuncArgTwoKinds)

Fixes to testing printing.

976ece7

Fix to pushCaseAppArgIn rewrite.

0460d69

lowered step limit for forallWithPolyFuncArg test

76d5a76

changes to support --no-duplicate-outputs

c450e92

Default config and Bindings Named instance for duplicate outputs option

d0af9d4

No extra checkmarks when validating with --no-duplicate-outputs option

4159b87

NO crash on GHC error. Report error and continue attempting to valida…

c89d957

…te outputs.

undefined app rewrite. avoids some validation SourceErrors

39ba0f0

Typeclass dicts have special handling. Can load into validation and r…

b53beda

…eport to user. Some issues

Infixing typeclass methods in Haskell printing

f9beadb

Initial handling for single method dicts

e97ce1f

ASTContainer instance for StateDiff, full tyVarSubst in evalCase bran…

2049438

…ch that handles gen instances

Tests work with ValidateRes

45f47bb

Always require parentheses around Haskell Cases. Required for some tc…

7b3836d

… outputs

Clearer test cases, some differences between validation and test suite

a2f3dff

validateStates declares gen ADTs before gen instances

ec53cfd

Fix to allow compilation for untested modules

d74f269

Comments added while writing report

123ca7d

New type class rewrite in subModel

44954b3

JacobGH2 requested a review from BillHallahan May 13, 2026 00:44

BillHallahan requested changes May 18, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

More complete RankNTypes support#494

More complete RankNTypes support#494
JacobGH2 wants to merge 86 commits into
masterfrom
gen_tc_instances

JacobGH2 commented May 13, 2026

Uh oh!

BillHallahan May 17, 2026

Uh oh!

BillHallahan May 17, 2026

Uh oh!

BillHallahan May 17, 2026

Uh oh!

JacobGH2 May 19, 2026

Uh oh!

BillHallahan May 17, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

BillHallahan May 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

JacobGH2 commented May 13, 2026

Changes (can point to place in code if more information is needed)

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants