h$-f     None#$'(./5> !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~None#$'(./5>None#$'(./5> typeletLHS should always be a variabletypeletThe LHS should be a skolem variableAs for as ghc is concerned, the LHS should be an opaque type variable with unknown value (only the plugin knows); certainly, ghc should not try to unify it with anything.typeletParse successfultypeletDifferent constraint than we're looking for (does not imply an error)typeletConstraint of the shape we're looking for, but something is wrongtypelet>Apply parser to each value in turn, bailing at the first errortypelet Variation on  which rules out the error casetypelet/Bundle the parse result with the original valuetypeletParse Equal constraints Kind-correct Equal? constraints of any form are ok, so this cannot return errors.typeletEvidence for an Equal constraintTODO: should we worry about producing an evidence term that prevents floating stuff out of scope...? (the whole "coercions cannot simply be zapped" thing) See also  typeletCycle in a graphtypelet!Construct idempotent substitutionTODO: Not entirely sure if this is correct, might be too simplistic and/or an abuse of the ghc API; it is a whole lot simpler than  niFixTCvSubst, which is disconcerning. However, it seems to work for the examples so far; perhaps our use case is simpler? Needs more thought.typeletFormat a cycle We (arbitrarily) pick the first - in the cycle for the location of the error.None#$'(./5> ;None#$'(./5> typeletUsed together with  - to pair a type-level let binding with a castSee   for details.typelet is used along with  & to introduce type-level let bindings.See   for more information.typelet-(Nominal) type equality, up to type-level letThis is a class without any definitions; 'Equal a b' is instead proved by the plugin. Suppose we have a bunch of type-level let constraints in scope Let x1 t1 Let x2 t2 ...Then if  is the corresponding idempotent substitution, two types a and b are considered  if (a) and (b) are nominally equal.typelet Type-level let A constraint Let x t where x' is an (existential) type variable and t; is an arbitrary type represents a type-level let binding  let x = t.o Introduction form3Type-level let bindings should be introduced using  ) or its slightly higher level cousin,  .o Elimination form!To eliminate type-level let, use  . typeletType-safe cast, using  as the notion of equalitySee comments for . typelet2Primitive way to introduce type-level let binding.Usage: .case letT (Proxy @t) of LetT (_ :: Proxy x) ->)This introduces a type-level let binding x = t. typelet CPS form of  *While this is more convenient to use, the r6 parameter itself requires careful thought; see also . typelet)Pair a type-level let binding with a cast)Often when we introduce a type-level let x = t", we then want to cast some term e :: t to a term e :: x ; function  ) does these two things in one operation.>If we did the above as written, however, we would have a term e :: x where we know nothing about x at all (unless we cast again). This is typically not useful; instead, we go from a term e :: f t to a term e :: f x, let-binding the type index t but not the functor f. typelet CPS form of  See also comments for  .typeletDual to  Where   takes an existing value and then  introduces a type variable,  is used to produce a value and then  eliminate a type variable.*Consider constructing a heterogenous list  [x, y, z]. Without the typelet( library this might look something like hlist :: HList '[X, Y, Z] hlist = HCons @X @'[Y, Z] x $ HCons @Y @'[ Z] y $ HCons @Z @'[ ] z $ HNil/The problem here is that tail list argument to HCons9, and causes this example to be quadratic in size. With letAs' we could write this as hlist :: HList '[X, Y, Z] hlist = letAs' (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -> letAs' (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -> letAs' (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -> castEqual xs0Here we are using letAs' to introduce a type variable for each partial list, thereby avoiding the repeated lists in the type arguments. However, if we write it like this, there is an additional repeated list in the implicit continuation type argument r to letAs'; making that argument explicit, the above code is really this: hlist :: HList '[X, Y, Z] hlist = letAs' @(HList '[X, Y, Z]) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -> letAs' @(HList '[X, Y, Z]) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -> letAs' @(HList '[X, Y, Z]) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -> castEqual xs0The solution is to introduce one more type variable for the whole list, and use that as the top-level: hlist :: HList '[X, Y, Z] hlist = constructLet $ \(_ :: Proxy ts) -> letAs' @(HList ts) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -> letAs' @(HList ts) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -> letAs' @(HList ts) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -> castEqual xs0Note that none of these type arguments are necessary; we merely showed them to illustrate what is going on. The final example can be written as shown below, and will be linear in size: hlist :: HList '[X, Y, Z] hlist = constructLet $ letAs' (HCons z Nil) $ \xs2 -> letAs' (HCons y xs2) $ \xs1 -> letAs' (HCons x xs1) $ (xs0 -> castEqual xs0typelet Reflexivity A constraint Let x t, where x/ is an existential (skolem) type variable and t+ is an arbitrary type, models a type-level  let x = t'. There is only a single instance for Let*: reflexivity (a type is equal to itself).&User code normally does not work with Let< directly, but instead uses one of the introduction forms (  and   ) which take care to introduce Let& constraints of the right shape. When Let constraints are introduced manually, the plugin will report a type error if0The left-hand side is not a skolem type variable,The set of let-bindings in scope are cyclic.    None#$'(./5>S           !"#"$"%"&"'"(")"*"+","-"."/"0"1"2"3"4"5"6"7898:8;8<8=8>8?8@8A8B8C8D8E8F8G8HIJKLKMKNKOKPKQKRKSKTKUKUVWXYZY[YYY\Y]^^_`abacadaeafaghihjklkmknkokpkqkrksktkudvewexeyeze{e|e}e~eeeeeeeeeeddddhhcc_ccccedY$typelet-0.1.2-6sPf7NNwtCtBdrZO6jvvZmTypeLet.UserAPITypeLet.PluginTypeLet.Plugin.GhcTcPluginAPITypeLet.Plugin.NameResolutionTypeLet.Plugin.ConstraintsTypeLet.Plugin.SubstitutionTypeLetbase Data.ProxyProxypluginLetAsLetTEqualLet castEqualletTletT'letAsletAs' constructLet$fLetkaa Debug.TracetraceghcTcMTypewriteMetaTyVarisFilledMetaTyVar_maybe TcRnMonadnewName TcRnTypesTcGblEnv TcTyThing ConstraintbumpCtLocDepthctEvExprctEqRel ctFlavourctPredctOriginctLoc ctEvidencemkNonCanonicalCtQCInstTcEvDest EvVarDestHoleDest CtEvidence ctev_destctev_loc ctev_pred ctev_evar CtFlavourCtLocHscTypes FindResultNotFound FoundMultipleFound NoPackagefr_suggestions fr_unusablesfr_pkgs_hiddenfr_mods_hiddenfr_pathsfr_pkg MonadThings lookupTyCon lookupDataCon lookupThinglookupIdTcOriginCtOrigin TcEvidence evDataConAppevCast evCoercion lookupEvBind EvBindsVarEvBindeb_lhseb_rhsEvTermEvExprInstEnvInstEnvsTcLclEnvTcType isMetaTyVar isSkolemTyVarMetaInfoTcLevel FamInstEnvId mkLocalIdCoreSynExprVarCoercionTypeCoreBndrCoreExprDataConpromoteDataCon classDataCon Predicate mkClassPredclassifyPredTypePred ForAllPred IrredPred ClassPredEqPredEqRelNomEqReprEqmkPrimEqPredRoleisCoercionTy_maybe mkCoercionTytyConAppTyCon_maybetyConAppTyConPicky_maybe mkTyConApp isStrLitTy mkStrLitTy isNumLitTy mkNumLitTy splitAppTyssplitAppTy_maybemkAppTysgetTyVar_maybe isTyVarTy TyCoSubstsubstTy substTyWith zipTvSubstTCvSubstTyCoFVstyCoVarsOfTypeTyCoRep mkTyConTymkPiTysmkPiTy mkForAllTys mkTyVarTys mkTyVarTy CoercionHole ch_co_varch_ref isCoercionTymkAppTyeqTypesplitTyConApp_maybeVarSet elemVarSetClass classTyConFunDepmkReflComkUnivComkSymCo mkTransCoCoAxiomRolePhantomNominalRepresentationalmkTyVarCoVarTyVarTcTyVarEvVar mkForAllTyTyThingUnivCoProvenancePredTypeKindOccNamemkClsOccmkTcOcc mkTyVarOcc mkDataOccmkVarOccModulestringToUnitIdunitIdFS mkModuleNameUniqDFMelemUDFMlookupUDFM_Directly lookupUDFMUniqFM listToUFMemptyUFMUnique BasicTypes isPromotedArity PromotionFlag NotPromoted IsPromotedBoxityBoxedUnboxed TupleSortConstraintTuple BoxedTuple UnboxedTupleSrcLocgetLocunLoc GenLocatedLLocated RealLocated MetaDetails OutputablepprDebugAndThenassertPprPanic pprSTracepprTraceException pprTraceIt pprTraceWith pprTraceMpprTrace pprTraceDebug pprPgmErrorpprSorrypprPanic callStackDocdoOrDoesisOrArepluralspeakNOfspeakNspeakNth intWithCommasquotedListWithNorquotedListWithOr pprQuotedList interpp'SP interppSP pprWithBars pprWithCommaspprFilePathStringpprFastFilePath pprInfixVar pprPrefixVar pprPrimWord64 pprPrimInt64 pprPrimWord pprPrimInt pprPrimCharprimWord64SuffixprimInt64SuffixprimWordSuffixprimDoubleSuffix primIntSuffixprimFloatSuffixprimCharSuffix pprHsBytes pprHsString pprHsCharkeywordcolouredppUnlessppWhen punctuate hangNotEmptyhangfcatfsepcatsepvcathsephcat$+$$$<+><>nest unicodeSyntaxbulletkindType forAllLitrbracelbracerbracklbrackrparenlparenvbardot underscorespaceequalscoloncommasemilarrowttarrowttlarrowtarrowtdarrowlarrowarrowdcolon blankLinequotescparen angleBrackets doubleQuotesquotebracketsbracesparens doublePrecwordrationaldoublefloatintegerintztextptextftextcharempty docToSDocisEmptyshowSDocDumpOneLineshowSDocOneLinerenderWithStyle showSDocDebug showSDocDumpshowSDocForUsershowSDocUnqualshowPprshowSDoc mkCodeStylepprCodebufLeftRenderSDoc printForCprintForUserPartWay printForUser printSDocLn printSDoc whenPprDebug ifPprDebug getPprDebug userStyle debugStyle dumpStyleasmStyle codeStyle queryQual qualPackage qualModulequalNameupdSDocDynFlagssdocWithPlatformsdocWithDynFlags getPprStyle pprSetDepth pprDeeperList pprDeeperwithPprStyleDoc withPprStyleinitSDocContextsetStyleColoured mkUserStylecmdlineParserStyle mkErrStyledefaultErrStyle mkDumpStyledefaultDumpStyledefaultUserStyle neverQualify alwaysQualifyreallyAlwaysQualifyneverQualifyPackagesalwaysQualifyPackagesneverQualifyModulesalwaysQualifyModulesneverQualifyNamesalwaysQualifyNamesreallyAlwaysQualifyNamesPprStyle CodeStyleCStyleAsmStyleDepth AllTheWayPartWayPrintUnqualified QueryQualifyqueryQualifyPackagequeryQualifyNamequeryQualifyModuleQueryQualifyNameQueryQualifyModuleQueryQualifyPackage QualifyNameNameNotInScope2NameNotInScope1 NameUnqualNameQualpprpprPrec BindingSiteLetBind CasePatBind LambdaBindCaseBindOutputableBndrbndrIsJoin_maybe pprInfixOccpprBndr pprPrefixOcc ModuleNameUnitId FastStringfsLitunpackFSTyCon PlainPanic assertPanicpgmErrorsorrypanicshowSDocUnsafe warnPprTracetextSDocrunSDocName/ghc-tcplugin-api-0.8.0.0-ITI5dz7KkQpKzXhGV4x9WnGHC.TcPlugin.APImkVisFunTysManymkInvisFunTysManymkVisFunTyManymkInvisFunTyManymkUncheckedIntExprmkTyFamAppReductionmkPluginUnivEvTermmkPluginUnivCo setEvBindnewCoercionHolenewEvVarsetCtLocRewriteM setCtLocMrewriteEnvCtLocnewGiven newWantedzonkCt zonkTcTypeisTouchableTcPluginM newFlexiTyVar newUniquematchFamgetFamInstEnvs getInstEnvsgetEnvs tcLookupIdtcLookuptcLookupGlobal tcLookupClasstcLookupDataCon tcLookupTyCon lookupOrigfindImportedModule pkgQual_pkg tcPluginTrace tcPluginIOPkgQualOtherPkg NoPkgQualThisPkgGHC.TcPlugin.API.InternalmkTcPluginErrorTy mkTcPlugin askRewriteEnv askDeriveds askEvBinds TcPluginStageRewriteSolveStopInitTcPluginSolverTcPluginRewriterTcPlugintcPluginRewrite tcPluginStop tcPluginInit tcPluginSolve TcPluginM MonadTcPluginMonadTcPluginWorkTcPluginErrorMessage:-::|:Txt PrintTypeGHC.TcPlugin.API.Internal.Shim RewriteEnvTcPluginSolveResultTcPluginContradiction TcPluginOkTcPluginRewriteResultTcPluginNoRewriteTcPluginRewriteTotcPluginReductiontcRewriterWanteds(GHC.TcPlugin.API.Internal.Shim.Reduction ReductionreductionCoercionreductionReducedType ResolvedNamesclsEqualclsLet resolveNamesNonVariableLHS NonSkolemLHSParseOk ParseNoMatch ParseErrorparseAll parseAll'withOrig parseEqual evidenceEqual InvalidLet ParseResultCEqual equalKindequalLHSequalRHSCLetletKindletLHSletRHSparseLet formatCLetformatInvalidLetCycle letsToSubstformatLetCycle