h$#     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 r, parameter itself requires careful thought. 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  .typelet 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>n           !"!#!$!%!&!'!(!)!*!+!,!-!.!/!0!1!2!3!4!5!678797:7;7<7=7>7?7@7A7B7C7D7E7F7GHIJKJLJMJNJOJPJQJRJSJTJTUVWXYXZXXX[X\]]^_`a`b`c`d`e`fghgijkjljmjnjojpjqjrjsjtcudvdwdxdydzd{d|d}d~ddddddddccccggbb^bbbbdcX&typelet-0.1.1.0-8KlVVeDlATm6teLcSnjzCyTypeLet.UserAPITypeLet.PluginTypeLet.Plugin.GhcTcPluginAPITypeLet.Plugin.NameResolutionTypeLet.Plugin.ConstraintsTypeLet.Plugin.SubstitutionTypeLetbase Data.ProxyProxypluginLetAsLetTEqualLet castEqualletTletT'letAsletAs'$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 mkNumLitTysplitAppTy_maybemkAppTysgetTyVar_maybe isTyVarTy TyCoSubstsubstTy substTyWith zipTvSubstTCvSubstTyCoFVstyCoVarsOfTypeTyCoRep mkTyConTymkPiTysmkPiTy mkForAllTys mkTyVarTys mkTyVarTy CoercionHole ch_co_varch_ref isCoercionTymkAppTyeqTypesplitTyConApp_maybeVarSet elemVarSetClass classTyConFunDepmkReflComkUnivComkSymCo mkTransCoCoAxiomRolePhantomNominalRepresentationalmkTyVarCoVarTyVarTcTyVarEvVar mkForAllTyTyThingUnivCoProvenancePredTypeKindOccNamemkClsOccmkTcOcc mkTyVarOcc mkDataOccmkVarOccModule 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 ModuleName FastStringfsLitTyCon PlainPanic assertPanicpgmErrorsorrypanicshowSDocUnsafe warnPprTracetextSDocrunSDocName/ghc-tcplugin-api-0.7.1.0-E8XW7069dIqEmJZqRf0icqGHC.TcPlugin.APImkVisFunTysManymkInvisFunTysManymkVisFunTyManymkInvisFunTyManymkUncheckedIntExprmkTyFamAppReductionmkPluginUnivEvTermmkPluginUnivCo setEvBindnewCoercionHolenewEvVarsetCtLocRewriteM setCtLocMrewriteEnvCtLocnewGiven newWantedzonkCt zonkTcTypeisTouchableTcPluginM newFlexiTyVar newUniquematchFamgetFamInstEnvs getInstEnvsgetEnvs tcLookupIdtcLookuptcLookupGlobal tcLookupClasstcLookupDataCon tcLookupTyCon lookupOrigfindImportedModule tcPluginTrace tcPluginIOGHC.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