h*7(     0.1.4 Safe-Inferred%&)*019 !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-Inferred%&)*019 Safe-Inferred%&)*019 g 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%&)*019$typelet'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%&)*019( 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%&)*019(         !"#$%&'()*+,-.-/-0-1-2-3-456789:;<"=">?@%A%BCDEFEGEHEEEIJKLMNOPQRQSQTQUVWXYZ[Z\Z]^_^`^a^b^cde%f%ghihjhkllmnopoqorosotouovowxyxyxzx{J|J}J~JJCCC)))))))))))))))++5COOQQVVVZd99999%oodC"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""$typelet-0.1.4-GnKT7zTkLG76RaskzCSheSTypeLet.UserAPITypeLet.PlugintypeletTypeLet.Plugin.GhcTcPluginAPITypeLet.Plugin.NameResolutionTypeLet.Plugin.ConstraintsTypeLet.Plugin.SubstitutionTypeLetbase Data.ProxyProxypluginLetAsLetTEqualLet castEqualletTletT'letAsletAs' constructLet$fLetkaaghcGHC.Core.TyConTyConGHC.Unit.TypesModuleGHC.Core.TyCo.RepTypeCoercionGHC.Types.UniqueUniqueGHC.Utils.OutputableSDocKind GHC.Types.VarIdGHC.Tc.Solver.InertSetInertSet GHC.Tc.TypesTcGblEnvGHC.Data.FastString FastStringLanguage.Haskell.Syntax.BasicRoleNominalRepresentationalPhantomBoxityBoxedUnboxed#Language.Haskell.Syntax.Module.Name ModuleNameGHC.Tc.Types.OriginCtOriginGHC.Types.Name.OccurrenceOccNameUnitIdunitIdFS OutputablepprGHC.Types.NameNameTcTyVarTyVarGHC.Tc.Utils.TcType MetaDetailsGHC.CoreCoreExprCoreBndrExprVarGHC.Types.TyThingTyThingPredTypeMultUnivCoProvenanceGHC.Types.Unique.FMUniqFMGHC.Types.SrcLoc RealLocatedLocated GenLocatedLGHC.Types.Unique.DFMUniqDFMGHC.Types.PkgQualPkgQualLanguage.Haskell.Syntax.Type PromotionFlag NotPromoted IsPromotedGHC.Types.Basic TupleSort BoxedTuple UnboxedTupleConstraintTupleArityGHC.Core.DataConDataConEvVarCoVarGHC.Core.ClassFunDepClass classTyCon CoercionHole ch_co_varch_refGHC.Core.PredicateEqRelNomEqReprEqPred ClassPredEqPred IrredPred ForAllPredGHC.Core.Reduction ReductionreductionCoercionreductionReducedType MonadThings lookupThinglookupId lookupDataCon lookupTyConGHC.Core.FamInstEnv FamInstEnvTcLevelMetaInfoTcType TcTyThingTcLclEnvGHC.Tc.Types.EvidenceEvExprEvTermEvBindeb_lhseb_rhs EvBindsVarGHC.Core.InstEnvInstEnvsGHC.Unit.Finder.Types FindResultFound NoPackage FoundMultipleNotFoundfr_pathsfr_pkgfr_mods_hiddenfr_pkgs_hidden fr_unusablesfr_suggestionsGHC.Tc.Types.ConstraintCtLoc CtFlavour CtEvidence ctev_pred ctev_evarctev_loc ctev_destTcEvDest EvVarDestHoleDestQCInstCtTcPluginRewriteResultTcPluginNoRewriteTcPluginRewriteTotcPluginReductiontcRewriterNewWantedsTcPluginSolveResult TcPluginOkTcPluginContradictiontcPluginInsolubleCtstcPluginSolvedCtstcPluginNewCts0ghc-tcplugin-api-0.11.0.0-AUb9nqZrIGoDfhcM40UAT5GHC.TcPlugin.API.InternalTcPlugin tcPluginInit tcPluginSolvetcPluginRewrite tcPluginStop TcPluginMTcPluginRewriterTcPluginSolver RewriteEnvGHC.Tc.Solver.MonadTcSTcPluginErrorMessageTxt PrintType:|::-:MonadTcPluginWork MonadTcPlugin TcPluginStageStopInitSolveRewrite GHC.Core.TypeManyTyOneTyGHC.TcPlugin.API newUnique mkTyConTyGHC.Utils.Panic.PlainpanicunpackFSfsLit mkModuleNameGHC.Utils.PanicpprPanic isMetaTyVar mkForAllTyemptyUFM listToUFMunLocgetLoc lookupUDFMlookupUDFM_DirectlyelemUDFMstringToUnitId isPromotedpromoteDataConmkVarOcc mkDataOcc mkTyVarOccmkTcOccmkClsOccmkTyVargetTyVar_maybetyConAppTyCon_maybesplitTyConApp_maybe mkCoercionTy mkTyConAppmkAppTy isCoercionTyGHC.Core.Coercion mkTransComkSymComkUnivComkReflCo mkTyVarTy mkTyVarTys mkInvisFunTy mkInvisFunTysmkVisFunTyManymkVisFunTysMany mkForAllTysmkPiTymkPiTys isTyVarTymkAppTyssplitAppTy_maybe splitAppTys mkNumLitTy isNumLitTy mkStrLitTy isStrLitTytyConAppTyConPicky_maybeisCoercionTy_maybeGHC.Core.TyCo.CompareeqTypemkPrimEqPredRoleclassifyPredType mkClassPred classDataCon GHC.Types.Id mkLocalId isSkolemTyVar lookupEvBind evCoercionevCast evDataConAppmkNonCanonical ctEvidencectLocctOriginctPred ctFlavourctEqRelctEvExprbumpCtLocDepthfindImportedModulegetEnvsGHC.Tc.Utils.MonadnewName readTcRef writeTcRef setCtLocMgetTcEvBindsMapsetTcEvBindsMapnewEvVar newWantednewCoercionHoleGHC.Tc.Utils.TcMTypeisFilledMetaTyVar_maybewriteMetaTyVar newFlexiTyVarzonkCt zonkTcType lookupOrigtcLookupGlobaltcLookupDataCon tcLookupClass tcLookupTyContcLookup tcLookupId getInstEnvsgetFamInstEnvs setEvBindmatchFam tcPluginIO tcPluginTraceisTouchableTcPluginMnewGiven askEvBinds askDeriveds askRewriteEnv mkTcPluginmkTcPluginErrorTypkgQualToPkgName resolveImportrewriteEnvCtLocsetCtLocRewriteMmkPluginUnivComkPluginUnivEvTermmkTyFamAppReduction getInertSet setInertSetIsDocLinevcat$$linelines_dualDocIsLinetext<>char<+>ftextztexthcathsepsepfsepdualLineIsOutputemptydocWithContextHDocHLineOutputableBndrpprBndr pprPrefixOcc pprInfixOccbndrIsJoin_maybe BindingSite LambdaBindCaseBind CasePatBindLetBindPDoc OutputablePpdoc SDocContextSDC sdocStyle sdocColSchemesdocLastColoursdocShouldUseColorsdocDefaultDepthsdocLineLengthsdocCanUseUnicodesdocHexWordLiterals sdocPprDebugsdocPrintUnicodeSyntaxsdocPrintCaseAsLetsdocPrintTypecheckerElaborationsdocPrintAxiomIncompssdocPrintExplicitKindssdocPrintExplicitCoercionssdocPrintExplicitRuntimeRepssdocPrintExplicitForallssdocPrintPotentialInstancessdocPrintEqualityRelationssdocSuppressTickssdocSuppressTypeSignaturessdocSuppressTypeApplicationssdocSuppressIdInfosdocSuppressCoercionssdocSuppressCoercionTypessdocSuppressUnfoldingssdocSuppressVarKindssdocSuppressUniquessdocSuppressModulePrefixessdocSuppressStgExtssdocSuppressStgRepssdocErrorSpanssdocStarIsTypesdocLinearTypessdocListTuplePunssdocPrintTypeAbbreviationssdocUnitIdForUser QualifyName NameUnqualNameQualNameNotInScope1NameNotInScope2IsEmptyOrSingleton PromotedItemPromotedItemListSyntaxPromotedItemTupleSyntaxPromotedItemDataConPromotionTickContext PromTickCtxptcListTuplePunsptcPrintRedundantPromTicksQueryPromotionTickQueryQualifyPackageQueryQualifyModuleQueryQualifyName NamePprCtx QueryQualifyqueryQualifyNamequeryQualifyModulequeryQualifyPackagequeryPromotionTickDepth AllTheWayPartWay DefaultDepthPprStylePprUserPprDumpPprCodeparensisEmptyptextsemicommacolonspaceequalslparenrparenlbrackrbracklbracerbraceintintegerfloatdoublerationalquotesquote doubleQuotesbracketsbracesnesthang hangNotEmpty punctuate$+$catfcatisListEmptyOrSingletonreallyAlwaysQualifyNamesalwaysQualifyNamesneverQualifyNamesalwaysQualifyModulesneverQualifyModulesalwaysQualifyPackagesneverQualifyPackagesalwaysPrintPromTickreallyAlwaysQualify alwaysQualify neverQualifydefaultUserStyledefaultDumpStyle mkDumpStyledefaultErrStyle mkErrStylecmdlineParserStyle mkUserStyle withUserStyle withErrStylesetStyleColouredrunSDocdefaultSDocContexttraceSDocContext withPprStyle pprDeeper pprDeeperList pprSetDepth getPprStylesdocWithContext sdocOptionupdSDocContextqualName qualModule qualPackagepromTick queryQual codeStyle dumpStyle userStyle getPprDebug ifPprDebug whenPprDebug printSDoc printSDocLnbufLeftRenderSDocpprCoderenderWithContextshowSDocOneLineshowSDocUnsafe showPprUnsafepprDebugAndThen docToSDocword doublePrec angleBracketscparen blankLinedcolonarrowlollipoplarrowdarrowarrowtlarrowtarrowttlarrowttlambda underscoredotvbar forAllLitbullet unicodeSyntaxppWhenppUnless ppWhenOptionppUnlessOptioncolouredkeyword pprModuleName pprHsChar pprHsString pprHsBytesprimCharSuffixprimFloatSuffix primIntSuffixprimDoubleSuffixprimWordSuffixprimInt8SuffixprimWord8SuffixprimInt16SuffixprimWord16SuffixprimInt32SuffixprimWord32SuffixprimInt64SuffixprimWord64Suffix pprPrimChar pprPrimInt pprPrimWord pprPrimInt8 pprPrimInt16 pprPrimInt32 pprPrimInt64 pprPrimWord8 pprPrimWord16 pprPrimWord32 pprPrimWord64 pprPrefixVar pprInfixVarpprFastFilePathpprFilePathString pprWithCommas pprWithBarsspaceIfSingleQuote interppSP interpp'SP interpp'SP' pprQuotedListquotedListWithOrquotedListWithNor intWithCommasspeakNthspeakNspeakNOfpluralsingularisOrAredoOrDoes itsOrTheir thisOrThese hasOrHavebPutHDocGHC.Core.TyCo.SubstSubstsubstTy substTyWith zipTvSubstGHC.Types.Var.Set elemVarSetGHC.Core.TyCo.FVstyCoVarsOfType ResolvedNamesclsEqualclsLet resolveNamesNonVariableLHS NonSkolemLHSParseOk ParseNoMatch ParseErrorparseAll parseAll'withOrig parseEqual evidenceEqualCEqual equalKindequalLHSequalRHSCLetletKindletLHSletRHS ParseResult InvalidLetparseLet formatCLetformatInvalidLetCycle letsToSubstinorderformatLetCyclesolvesimplifyGivenssimplifyWanteds