h&7V(      Safe-Inferred%&)*018 !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-Inferred%&)*018b Safe-Inferred%&)*018  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  (x := xT)The required assignment ordering is then obtained by topological sort.typeletFormat a cycle We (arbitrarily) pick the first - in the cycle for the location of the error. Safe-Inferred%&)*018typelet'Main interface to constraint resolutionNOTE: For now we are completely ignoring the derived constraints.typeletSimplify givensWe (currently?) never simplify any givens, so we just two empty lists, indicating that there no constraints were removed and none got added.typeletSimplify wanteds;This function provides the key functionality of the plugin. We resolve Equal constraints to nominal equality constraints: we want cast to resolve Let( bindings, but not additionally work as coerce.typelet'Result of name resolution (during init)typeletGiven constraintstypelet'Result of name resolution (during init)typeletGiven constraintstypeletWanted constraints Safe-Inferred%&)*018(# 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 discussion of  for additional information.Note: without additional  constraints in scope, 8 constraints simply resolve to unification constraints:(castEqual :: Int -> Bool) 1...!...Couldn't match...Int...Bool...... 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 if)The left-hand side is not a type variable8let aux :: Let Int Int => () ; aux = castEqual () in aux......Let with non-variable LHS......:{  \(x :: a) -> let y :: Let a Int => a y = castEqual (1 :: Int) in y:}......Let with non-variable LHS......,The set of let-bindings in scope are cyclic.:{5 let cycle :: (Let a b, Let b a) => (a, b) -> (a, b)/ cycle (a, b) = (castEqual b, castEqual a) in cycle ('a', 'b'):}...3...Cycle in type-level let bindings: a := b, b := a...     Safe-Inferred%&)*018(           ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 567898:8:8;8<8=8>8?8@8A8BCDEFGFHFIFJKLKMKNKOKPQRSTSUSVSWSXSYZ[Z\Z]Z^Z_Z`ZaZbZcZdZefghijkjljmjnjojpjqjrjsjtuvwxwywzw{w|w}w~wwwwwwuuuuffwwwwwwVWKFF$typelet-0.1.3-1B5WSU6KhxZHz4l0C9FF0gTypeLet.UserAPITypeLet.PluginTypeLet.Plugin.GhcTcPluginAPITypeLet.Plugin.NameResolutionTypeLet.Plugin.ConstraintsTypeLet.Plugin.SubstitutionTypeLetbase Data.ProxyProxypluginLetAsLetTEqualLet castEqualletTletT'letAsletAs' constructLet$fLetkaaghcGHC.Tc.Utils.TcMTypewriteMetaTyVarisFilledMetaTyVar_maybeGHC.Tc.Utils.MonadnewName GHC.Tc.Types TcTyThingTcGblEnvGHC.Tc.Types.ConstraintTcEvDest EvVarDestHoleDestQCInstCtLoc CtFlavour CtEvidence ctev_predctev_loc ctev_dest ctev_evarCtmkNonCanonicalctPredctOriginctLoc ctFlavour ctEvidencectEvExprctEqRelbumpCtLocDepthGHC.Tc.Types.OriginCtOriginGHC.Tc.Types.EvidenceEvTermEvExpr EvBindsVarEvBindeb_lhseb_rhs lookupEvBind evDataConApp evCoercionevCastGHC.Core.InstEnvInstEnvsTcLclEnvGHC.Tc.Utils.TcTypeTcTypeTcLevelMetaInfo isSkolemTyVarGHC.Types.TyThing MonadThings lookupTyCon lookupThing lookupDataConlookupId GHC.Types.Id mkLocalIdGHC.CoreExprVarTypeCoercionCoreExprCoreBndrGHC.Unit.Finder.Types FindResult fr_unusablesfr_suggestionsfr_pkgs_hiddenfr_pkgfr_pathsfr_mods_hiddenNotFound NoPackageFound FoundMultipleGHC.Core.DataCon classDataConGHC.Core.FamInstEnv FamInstEnvGHC.Core.PredicatePred IrredPred ForAllPred ClassPredEqPredEqRelNomEqReprEq mkClassPredclassifyPredTypeGHC.Core.CoercionmkPrimEqPredRole GHC.Core.TypetyConAppTyConPicky_maybe splitAppTyssplitAppTy_maybe mkStrLitTy mkNumLitTy mkCoercionTymkAppTys isTyVarTy isStrLitTy isNumLitTyisCoercionTy_maybegetTyVar_maybeeqTypeGHC.Core.TyCo.SubstTCvSubst zipTvSubst substTyWithsubstTyGHC.Core.TyCo.FVstyCoVarsOfTypeGHC.Core.TyCo.Rep CoercionHolech_ref ch_co_varmkVisFunTysManymkVisFunTyMany mkTyVarTys mkTyVarTymkPiTysmkPiTy mkForAllTysGHC.Core.ClassFunDepClass classTyConmkUnivCo mkTransComkSymComkReflCoGHC.Core.Coercion.AxiomRoleRepresentationalNominalPhantomGHC.Types.Var.Set elemVarSetGHC.Types.Name.OccurrencemkVarOcc mkTyVarOccmkTcOcc mkDataOccmkClsOcc GHC.Types.VarEvVarCoVarmkTyVarDataConpromoteDataContyConAppTyCon_maybesplitTyConApp_maybe mkTyConTy mkTyConAppmkAppTy isCoercionTyUnivCoProvenancePredTypeMultKind mkForAllTyTyThingGHC.Core.TyConTyCon MetaDetails isMetaTyVarGHC.Types.Basic TupleSort UnboxedTuple BoxedTupleConstraintTuple PromotionFlag IsPromoted NotPromotedBoxityBoxedUnboxedArity isPromotedTyVarTcTyVarIdGHC.Unit.TypesstringToUnitIdGHC.Unit.Module.Name mkModuleNameGHC.Types.NameNameGHC.Types.SrcLoc RealLocatedLocated GenLocatedLunLocgetLocGHC.Types.Unique.DFMUniqDFMlookupUDFM_Directly lookupUDFMelemUDFMGHC.Types.Unique.FMUniqFM listToUFMemptyUFMGHC.Types.UniqueUniqueGHC.Utils.PanicpprPanicGHC.Utils.OutputableQueryQualifyPackageQueryQualifyNameQueryQualifyModule QualifyName NameUnqualNameQualNameNotInScope1NameNotInScope2PrintUnqualifiedqueryQualifyPackagequeryQualifyName QueryQualifyqueryQualifyModulePDoc OutputablePpdocOutputableBndr pprPrefixOcc pprInfixOccbndrIsJoin_maybepprBndr Outputableppr LabelStyleAsmStyleCStyleDepthPartWay AllTheWay DefaultDepth BindingSiteLetBind LambdaBindCaseBind CasePatBindztextword withUserStyle withPprStyle withErrStyle whenPprDebugvcatvbar userStyleupdSDocContext unicodeSyntax underscorespeakNthspeakNOfspeakNspaceshowSDocUnsafeshowSDocOneLine showPprUnsafesetStyleColouredsepsemisdocWithContext sdocOptionrunSDocrparenrenderWithContextreallyAlwaysQualifyNamesreallyAlwaysQualifyrbrackrbracerationalquotesquotedListWithOrquotedListWithNorquote queryQual qualPackagequalName qualModule punctuateptext printSDocLn printSDocprimWordSuffixprimWord8SuffixprimWord64SuffixprimWord32SuffixprimWord16Suffix primIntSuffixprimInt8SuffixprimInt64SuffixprimInt32SuffixprimInt16SuffixprimFloatSuffixprimDoubleSuffixprimCharSuffix pprWithCommas pprWithBars pprSetDepth pprQuotedList pprPrimWord8 pprPrimWord64 pprPrimWord32 pprPrimWord16 pprPrimWord pprPrimInt8 pprPrimInt64 pprPrimInt32 pprPrimInt16 pprPrimInt pprPrimChar pprPrefixVar pprInfixVar pprHsString pprHsChar pprHsBytespprFilePathStringpprFastFilePath pprDeeperList pprDeeperpprCode ppWhenOptionppWhenppUnlessOptionppUnlesspluralparensneverQualifyPackagesneverQualifyNamesneverQualifyModules neverQualifynestmulArrow mkUserStyle mkErrStyle mkDumpStylelparenlollipoplbracklbracelarrowttlarrowtlarrowlambdakeyword itsOrTheirisOrAreisEmpty interppSP interpp'SP' interpp'SPinteger intWithCommasint ifPprDebughsephcat hangNotEmptyhang getPprStyle getPprDebugftextfsep forAllLitfloatfcatequalsempty dumpStyle doubleQuotes doublePrecdoubledot docToSDocdoOrDoesdefaultUserStyledefaultSDocContextdefaultErrStyledefaultDumpStyledcolondarrowcparencommacolouredcolon codeStylecmdlineParserStylecharcatbulletbufLeftRenderSDocbracketsbraces blankLineasmStylearrowttarrowtarrow angleBracketsalwaysQualifyPackagesalwaysQualifyNamesalwaysQualifyModules alwaysQualify<><+>$+$$$OccNameGHC.Data.FastString FastStringunpackFSfsLitGHC.Utils.Panic.PlainpanicUnitIdunitIdFSModule SDocContextsdocUnitIdForUsersdocSuppressVarKindssdocSuppressUniquessdocSuppressUnfoldingssdocSuppressTypeSignaturessdocSuppressTypeApplicationssdocSuppressTickssdocSuppressStgExtssdocSuppressModulePrefixessdocSuppressIdInfosdocSuppressCoercions sdocStylesdocStarIsTypesdocShouldUseColorsdocPrintUnicodeSyntaxsdocPrintTypecheckerElaborationsdocPrintTypeAbbreviationssdocPrintPotentialInstancessdocPrintExplicitRuntimeRepssdocPrintExplicitKindssdocPrintExplicitForallssdocPrintExplicitCoercionssdocPrintEqualityRelationssdocPrintCaseAsLetsdocPrintAxiomIncomps sdocPprDebugsdocLinearTypessdocLineLengthsdocLastColoursdocImpredicativeTypessdocHexWordLiteralssdocErrorSpanssdocDefaultDepth sdocColSchemeSDCsdocCanUseUnicodeSDocPprStylePprUserPprCodePprDumptext ModuleName0ghc-tcplugin-api-0.10.0.0-Iq8gG2Whuq3FGBMqE1YHKVGHC.TcPlugin.APImkTyFamAppReductionmkPluginUnivEvTermmkPluginUnivCo setEvBindnewCoercionHolenewEvVarsetCtLocRewriteM setCtLocMrewriteEnvCtLocnewGiven newWantedzonkCt zonkTcTypeisTouchableTcPluginM newFlexiTyVar newUniquematchFamgetFamInstEnvs getInstEnvsgetEnvs tcLookupIdtcLookuptcLookupGlobal tcLookupClasstcLookupDataCon tcLookupTyCon lookupOrigfindImportedModule resolveImportpkgQualToPkgName mkInvisFunTys mkInvisFunTy tcPluginTrace tcPluginIOOneTyManyTyPkgQualGHC.TcPlugin.API.InternalmkTcPluginErrorTy mkTcPlugin askRewriteEnv askDeriveds askEvBinds TcPluginStageRewriteSolveStopInitTcPluginSolverTcPluginRewriterTcPlugintcPluginRewrite tcPluginStop tcPluginSolve tcPluginInit TcPluginM MonadTcPluginMonadTcPluginWorkTcPluginErrorMessage:-::|:Txt PrintTypeGHC.TcPlugin.API.Internal.Shim RewriteEnvTcPluginSolveResultTcPluginContradiction TcPluginOkTcPluginRewriteResulttcRewriterNewWantedstcPluginReductionTcPluginNoRewriteTcPluginRewriteTo(GHC.TcPlugin.API.Internal.Shim.Reduction ReductionreductionReducedTypereductionCoercion ResolvedNamesclsEqualclsLet resolveNamesNonVariableLHS NonSkolemLHSParseOk ParseNoMatch ParseErrorparseAll parseAll'withOrig parseEqual evidenceEqual InvalidLet ParseResultCEqual equalKindequalLHSequalRHSCLetletKindletLHSletRHSparseLet formatCLetformatInvalidLetCycle letsToSubstinorderformatLetCyclesolvesimplifyGivenssimplifyWanteds