konn

{-# LANGUAGE ConstraintKinds, DataKinds, DeriveGeneric, DerivingVia    #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances   #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds, ScopedTypeVariables, StandaloneDeriving        #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators #-}
{-# LANGUAGE UndecidableInstances                                      #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Aeson.Generic.DerivingVia
     ( StrFun(..), Setting(..), SumEncoding'(..), DefaultOptions, WithOptions(..)
     , -- Utility type synonyms to save ticks (') before promoted data constructors

laughinghan

• any: magic, ill-behaved type that acts like a combination of never (the proper [bottom type]) and unknown (the proper [top type])
  • Anything except never is assignable to any, and any is assignable to anything at all.
  • Identities: any & AnyTypeExpression = any, any | AnyTypeExpression = any
  • Key TypeScript feature that allows for [gradual typing].
• unknown: proper, well-behaved [top type]
  • Anything at all is assignable to unknown. unknown is only assignable to itself (unknown) and any.
  • Identities: unknown & AnyTypeExpression = AnyTypeExpression, unknown | AnyTypeExpression = unknown

• Prefer over any whenever possible. Anywhere in well-typed code you're tempted to use any, you probably want unknown.

aaronmdjones

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

My resignation from freenode staff
==================================

I joined the freenode staff in March 2019 [1].

Before I joined the staff, Freenode Ltd was sold [2] to a person named
Andrew Lee as part of a sponsorship deal. The informal terms of that

TOTBWF

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []