diff --git a/compiler/concepts.nim b/compiler/concepts.nim
index 139f851667..af06f8cdca 100644
--- a/compiler/concepts.nim
+++ b/compiler/concepts.nim
@@ -11,7 +11,7 @@
 ## for details. Note this is a first implementation and only the "Concept matching"
 ## section has been implemented.
 
-import ast, semdata, lookups, lineinfos, idents, msgs, renderer, types, layeredtable
+import ast, astalgo, semdata, lookups, lineinfos, idents, msgs, renderer, types, layeredtable
 
 import std/intsets
 
@@ -19,7 +19,7 @@ when defined(nimPreviewSlimSystem):
   import std/assertions
 
 const
-  logBindings = false
+  logBindings = when defined(debugConcepts): true else: false
 
 ## Code dealing with Concept declarations
 ## --------------------------------------
@@ -70,26 +70,87 @@ proc semConceptDeclaration*(c: PContext; n: PNode): PNode =
 ## ----------------
 
 type
+  MatchFlags* = enum
+    mfDontBind  # Do not bind generic parameters
+    mfCheckGeneric  # formal <- formal comparison as opposed to formal <- operand
+  
   MatchCon = object ## Context we pass around during concept matching.
-    inferred: seq[(PType, PType)] ## we need a seq here so that we can easily undo inferences \
-      ## that turned out to be wrong.
+    bindings: LayeredIdTable
     marker: IntSet ## Some protection against wild runaway recursions.
     potentialImplementation: PType ## the concrete type that might match the concept we try to match.
     magic: TMagic  ## mArrGet and mArrPut is wrong in system.nim and
                    ## cannot be fixed that easily.
                    ## Thus we special case it here.
-    concpt: PType
+    concpt: PType  ## current concept being evaluated
+    depthCount = 0
+    flags: set[MatchFlags]
+    
+  MatchKind = enum
+    mkNoMatch, mkSubset, mkSame
+
+const
+  asymmetricConceptParamMods = {tyVar, tySink, tyLent, tyOwned, tyAlias, tyInferred} # param modifiers that to not have to match implementation -> concept
+  bindableTypes = {tyGenericParam, tyOr, tyTypeDesc}
+
+proc conceptMatchNode(c: PContext; n: PNode; m: var MatchCon): bool
+
+proc matchType(c: PContext; fo, ao: PType; m: var MatchCon): bool
+
+proc matchReturnType(c: PContext; f, a: PType; m: var MatchCon): bool
+
+proc processConcept(c: PContext; concpt, invocation: PType, bindings: var LayeredIdTable; m: var MatchCon): bool
 
 proc existingBinding(m: MatchCon; key: PType): PType =
   ## checks if we bound the type variable 'key' already to some
   ## concrete type.
-  for i in 0..<m.inferred.len:
-    if m.inferred[i][0] == key: return m.inferred[i][1]
-  return nil
+  result = m.bindings.lookup(key)
+  if result == nil:
+    result = key
 
-proc conceptMatchNode(c: PContext; n: PNode; m: var MatchCon): bool
+const
+    ignorableForArgType = {tyVar, tySink, tyLent, tyOwned, tyAlias, tyInferred}
 
-proc matchType(c: PContext; f, ao: PType; m: var MatchCon): bool
+proc unrollGenericParam(param: PType): PType =
+  result = param.skipTypes(ignorableForArgType)
+  while result.kind in {tyGenericParam, tyTypeDesc} and result.hasElementType and result.elementType.kind != tyNone:
+    result = result.elementType
+
+proc bindParam(c: PContext, m: var MatchCon; key, v: PType): bool {. discardable .} =
+  if v.kind == tyTypeDesc:
+    return false
+  var value = unrollGenericParam(v)
+  if value.kind == tyGenericParam:
+    value = existingBinding(m, value)
+    if value.kind == tyGenericParam:
+      if value.hasElementType:
+        value = value.elementType
+      else:
+        return true
+  if value.kind == tyStatic:
+    return false
+
+  if m.magic in {mArrPut, mArrGet} and value.kind in arrPutGetMagicApplies:
+    value = value.last
+  
+  let old = existingBinding(m, key)
+  if old != key:
+    # check previously bound value
+    if not matchType(c, old, value, m):
+      return false
+  elif key.hasElementType and key.elementType.kind != tyNone:
+    # check constaint
+    if matchType(c, unrollGenericParam(key), value, m) == false:
+      return false
+  
+  when logBindings: echo "bind table adding '", key, "', ", value
+  assert value != nil
+  assert value.kind != tyVoid
+  m.bindings.put(key, value)
+  return true
+
+proc defSignatureType(n: PNode): PType = n[0].sym.typ
+
+proc conceptBody*(n: PType): PNode = n.n.lastSon
 
 proc acceptsAllTypes(t: PType): bool=
   result = false
@@ -101,84 +162,152 @@ proc acceptsAllTypes(t: PType): bool=
     if not t.hasElementType or t.elementType.kind == tyNone:
       result = true
 
+proc procDefSignature(s: PSym): PNode {. deprecated .} = 
+  var nc = s.ast.copyNode()
+  for i in 0 .. 5:
+    nc.add s.ast[i]
+  nc
+
 proc matchKids(c: PContext; f, a: PType; m: var MatchCon, start=0): bool=
   result = true
-  for i in start..<f.kidsLen - ord(f.kind == tyGenericInst):
+  for i in start ..< f.kidsLen - ord(f.kind in {tyGenericInst, tyGenericInvocation}):
     if not matchType(c, f[i], a[i], m): return false
 
-proc matchType(c: PContext; f, ao: PType; m: var MatchCon): bool =
+iterator traverseTyOr(t: PType): PType {. closure .}=
+  for i in t.kids:
+    case i.kind:
+    of tyGenericParam:
+      if i.hasElementType:
+        for s in traverseTyOr(i.elementType):
+          yield s
+      else:
+        yield i
+    else:
+      yield i
+
+proc matchConceptToImpl(c: PContext, f, potentialImpl: PType; m: var MatchCon): bool =
+  assert not(potentialImpl.reduceToBase.kind == tyConcept)
+  let concpt = f.reduceToBase
+  if m.depthCount > 0:
+    # concepts that are more then 2 levels deep are treated like
+    # tyAnything to stop dependencies from getting out of control
+    return true
+  var efPot = potentialImpl
+  if potentialImpl.isSelf:
+    if m.concpt.n == concpt.n:
+      return true
+    efPot = m.potentialImplementation
+  
+  var oldBindings = m.bindings
+  m.bindings = newTypeMapLayer(m.bindings)
+  let oldPotentialImplementation = m.potentialImplementation
+  m.potentialImplementation = efPot
+  let oldConcept = m.concpt
+  m.concpt = concpt
+  
+  var invocation: PType = nil
+  if f.kind in {tyGenericInvocation, tyGenericInst}:
+    invocation = f
+  inc m.depthCount
+  result = processConcept(c, concpt, invocation, oldBindings, m)
+  dec m.depthCount
+  m.potentialImplementation = oldPotentialImplementation
+  m.concpt = oldConcept
+  m.bindings = oldBindings
+
+proc cmpConceptDefs(c: PContext, fn, an: PNode, m: var MatchCon): bool=
+  if fn.kind != an.kind:
+    return false
+  if fn[namePos].sym.name != an[namePos].sym.name:
+    return false
+  let
+    ft = fn.defSignatureType
+    at = an.defSignatureType
+  if ft.len != at.len:
+    return false
+  
+  for i in 1 ..< ft.n.len:
+    m.bindings = m.bindings.newTypeMapLayer()
+    
+    let aType = at.n[i].typ
+    let fType = ft.n[i].typ
+    
+    if aType.isSelf and fType.isSelf:
+      continue
+    
+    if not matchType(c, fType, aType, m):
+      m.bindings.setToPreviousLayer()
+      return false
+  result = true
+  if not matchReturnType(c, ft.returnType, at.returnType, m):
+    m.bindings.setToPreviousLayer()
+    result = false
+
+proc conceptsMatch(c: PContext, fc, ac: PType; m: var MatchCon): MatchKind =
+  # XXX: In the future this may need extra parameters to carry info for container types
+  if fc.n == ac.n:
+    # This will have to take generic parameters into account at some point
+    return mkSame
+  let
+    fn = fc.conceptBody
+    an = ac.conceptBody
+    sameLen = fc.len == ac.len
+  var match = false
+  for fdef in fn:
+    var cmpResult = false
+    for ia, ndef in an:
+      match = cmpConceptDefs(c, fdef, ndef, m)
+      if match:
+        break
+    if not match:
+      return mkNoMatch
+  return mkSubset
+
+proc matchType(c: PContext; fo, ao: PType; m: var MatchCon): bool =
   ## The heart of the concept matching process. 'f' is the formal parameter of some
   ## routine inside the concept that we're looking for. 'a' is the formal parameter
   ## of a routine that might match.
-  const
-    ignorableForArgType = {tyVar, tySink, tyLent, tyOwned, tyGenericInst, tyAlias, tyInferred}
   
-  var a = ao
+  var
+    a = ao
+    f = fo
   
-  case a.kind
-  of tyGenericParam:
-    let binding = m.existingBinding(a)
-    if binding != nil:
-      a = binding
-  else:
-    discard
+  if a.kind in bindableTypes:
+    a = existingBinding(m, ao)
+    if a == ao and a.kind == tyGenericParam and a.hasElementType and a.elementType.kind != tyNone:
+      a = a.elementType
   
+  if f.isConcept:
+    if a.acceptsAllTypes:
+      return false
+    if a.isConcept:
+      # if f is a subset of a then any match to a will also match f. Not the other way around
+      return conceptsMatch(c, a.reduceToBase, f.reduceToBase, m) >= mkSubset
+    else:
+      return matchConceptToImpl(c, f, a, m)
+  
+  result = false
+
   case f.kind
   of tyAlias:
     result = matchType(c, f.skipModifier, a, m)
   of tyTypeDesc:
     if isSelf(f):
+      let ua = a.skipTypes(asymmetricConceptParamMods)
       if m.magic in {mArrPut, mArrGet}:
-        result = false
         if m.potentialImplementation.reduceToBase.kind in arrPutGetMagicApplies:
-          m.inferred.add((a, last m.potentialImplementation))
+          bindParam(c, m, a, last m.potentialImplementation)
           result = true
+      #elif ua.isConcept:
+      #  result = matchType(c, m.concpt, ua, m)
       else:
-        result = matchType(c, a, m.potentialImplementation, m)
+        result = matchType(c, a.skipTypes(ignorableForArgType), m.potentialImplementation, m)
     else:
-      if a.kind == tyTypeDesc and f.hasElementType == a.hasElementType:
-        if f.hasElementType:
+      if a.kind == tyTypeDesc:
+        if not(a.hasElementType) or a.elementType.kind == tyNone:
+          result = true
+        elif f.hasElementType:
           result = matchType(c, f.elementType, a.elementType, m)
-        else:
-          result = true # both lack it
-      else:
-        result = false
-  of tyGenericInvocation:
-    result = false
-    if a.kind == tyGenericInst and a.genericHead.kind == tyGenericBody:
-      if sameType(f.genericHead, a.genericHead) and f.kidsLen == a.kidsLen-1:
-        result = matchKids(c, f, a, m, start=FirstGenericParamAt)
-  of tyGenericParam:
-    let ak = a.skipTypes({tyVar, tySink, tyLent, tyOwned})
-    if ak.kind in {tyTypeDesc, tyStatic} and not isSelf(ak):
-      result = false
-    else:
-      let old = existingBinding(m, f)
-      if old == nil:
-        if f.hasElementType and f.elementType.kind != tyNone:
-          # also check the generic's constraints:
-          let oldLen = m.inferred.len
-          result = matchType(c, f.elementType, a, m)
-          m.inferred.setLen oldLen
-          if result:
-            when logBindings: echo "A adding ", f, " ", ak
-            m.inferred.add((f, ak))
-        elif m.magic == mArrGet and ak.kind in {tyArray, tyOpenArray, tySequence, tyVarargs, tyCstring, tyString}:
-          when logBindings: echo "B adding ", f, " ", last ak
-          m.inferred.add((f, last ak))
-          result = true
-        else:
-          when logBindings: echo "C adding ", f, " ", ak
-          m.inferred.add((f, ak))
-          #echo "binding ", typeToString(ak), " to ", typeToString(f)
-          result = true
-      elif not m.marker.containsOrIncl(old.id):
-        result = matchType(c, old, ak, m)
-        if m.magic == mArrPut and ak.kind == tyGenericParam:
-          result = true
-      else:
-        result = false
-    #echo "B for ", result, " to ", typeToString(a), " to ", typeToString(m.potentialImplementation)
   of tyVar, tySink, tyLent, tyOwned:
     # modifiers in the concept must be there in the actual implementation
     # too but not vice versa.
@@ -186,91 +315,41 @@ proc matchType(c: PContext; f, ao: PType; m: var MatchCon): bool =
       result = matchType(c, f.elementType, a.elementType, m)
     elif m.magic == mArrPut:
       result = matchType(c, f.elementType, a, m)
-    else:
-      result = false
   of tyEnum, tyObject, tyDistinct:
-    result = sameType(f, a)
+    if a.kind in ignorableForArgType:
+      result = matchType(c, f, a.skipTypes(ignorableForArgType), m)
+    else:
+      result = sameType(f, a)
   of tyEmpty, tyString, tyCstring, tyPointer, tyNil, tyUntyped, tyTyped, tyVoid:
     result = a.skipTypes(ignorableForArgType).kind == f.kind
   of tyBool, tyChar, tyInt..tyUInt64:
     let ak = a.skipTypes(ignorableForArgType)
     result = ak.kind == f.kind or ak.kind == tyOrdinal or
-       (ak.kind == tyGenericParam and ak.hasElementType and ak.elementType.kind == tyOrdinal)
-  of tyConcept:
-    if a.kind == tyConcept and f.n == a.n:
-      result = true
-    elif m.concpt.size == szIllegalRecursion:
-      result = false
-    else:
-      let oldLen = m.inferred.len
-      let oldPotentialImplementation = m.potentialImplementation
-      m.potentialImplementation = a
-      m.concpt.size = szIllegalRecursion
-      let oldConcept = m.concpt
-      m.concpt = f
-      result = conceptMatchNode(c, f.n.lastSon, m)
-      m.potentialImplementation = oldPotentialImplementation
-      m.concpt = oldConcept
-      m.concpt.size = szUnknownSize
-      if not result:
-        m.inferred.setLen oldLen
-  of tyGenericBody:
-    var ak = a
-    if a.kind == tyGenericBody:
-      ak = last(a)
-    result = matchType(c, last(f), ak, m)
-  of tyCompositeTypeClass:
-    var ak = if a.kind == tyCompositeTypeClass: a.last else: a
-    result = matchType(c, last(f), ak, m)
-  of tyArray, tyTuple, tyVarargs, tyOpenArray, tyRange, tySequence, tyRef, tyPtr,
-     tyGenericInst:
-    # ^ XXX Rewrite this logic, it's more complex than it needs to be.
-    if f.kind == tyArray and f.kidsLen == 3:
+      (ak.kind == tyGenericParam and ak.hasElementType and ak.elementType.kind == tyOrdinal)
+  of tyArray, tyTuple, tyVarargs, tyOpenArray, tyRange, tySequence, tyRef, tyPtr:
+    if f.kind == tyArray and f.kidsLen == 3 and a.kind == tyArray:
       # XXX: this is a work-around!
       # system.nim creates these for the magic array typeclass
       result = true
     else:
-      result = false
       let ak = a.skipTypes(ignorableForArgType - {f.kind})
       if ak.kind == f.kind and f.kidsLen == ak.kidsLen:
         result = matchKids(c, f, ak, m)
-  of tyOr:
-    let oldLen = m.inferred.len
-    if a.kind == tyOr:
-      # say the concept requires 'int|float|string' if the potentialImplementation
-      # says 'int|string' that is good enough.
-      var covered = 0
-      for ff in f.kids:
-        for aa in a.kids:
-          let oldLenB = m.inferred.len
-          let r = matchType(c, ff, aa, m)
-          if r:
-            inc covered
+  of tyGenericInvocation, tyGenericInst:
+    result = false
+    let ea = a.skipTypes(ignorableForArgType)
+    if ea.kind in {tyGenericInst, tyGenericInvocation}:
+      var
+        k1 = f.kidsLen - ord(f.kind == tyGenericInst)
+        k2 = ea.kidsLen - ord(ea.kind == tyGenericInst)
+      if sameType(f.genericHead, ea.genericHead) and k1 == k2:
+        for i in 1 ..< k2:
+          if not matchType(c, f[i], ea[i], m):
             break
-          m.inferred.setLen oldLenB
-
-      result = covered >= a.kidsLen
-      if not result:
-        m.inferred.setLen oldLen
-    else:
-      result = false
-      for ff in f.kids:
-        result = matchType(c, ff, a, m)
-        if result: break # and remember the binding!
-        m.inferred.setLen oldLen
-  of tyNot:
-    if a.kind == tyNot:
-      result = matchType(c, f.elementType, a.elementType, m)
-    else:
-      let oldLen = m.inferred.len
-      result = not matchType(c, f.elementType, a, m)
-      m.inferred.setLen oldLen
-  of tyAnything:
-    result = true
+        result = true
   of tyOrdinal:
     result = isOrdinalType(a, allowEnumWithHoles = false) or a.kind == tyGenericParam
   of tyStatic:
-    result = false
     var scomp = f.base
     if scomp.kind == tyGenericParam:
       if f.base.kidsLen > 0:
@@ -279,8 +358,71 @@ proc matchType(c: PContext; f, ao: PType; m: var MatchCon): bool =
       result = matchType(c, scomp, a.base, m)
     else:
       result = matchType(c, scomp, a, m)
+  of tyGenericParam:
+    if a.acceptsAllTypes:
+      discard bindParam(c, m, f, a)
+      result = f.acceptsAllTypes
+    else:
+      result = bindParam(c, m, f, a)
+  of tyAnything:
+    result = true
+  of tyNot:
+    if a.kind == tyNot:
+      result = matchType(c, f.elementType, a.elementType, m)
+    else:
+      m.bindings = m.bindings.newTypeMapLayer()
+      result = not matchType(c, f.elementType, a, m)
+      m.bindings.setToPreviousLayer()
+  of tyAnd:
+    m.bindings = m.bindings.newTypeMapLayer()
+    result = true
+    for ff in traverseTyOr(f):
+      let r = matchType(c, ff, a, m)
+      if not r:
+        m.bindings.setToPreviousLayer()
+        result = false
+        break
+  of tyGenericBody:
+    var ak = a
+    if a.kind == tyGenericBody:
+      ak = last(a)
+    result = matchType(c, last(f), ak, m)
+  of tyCompositeTypeClass:
+    if a.kind == tyCompositeTypeClass:
+      result = matchKids(c, f, a, m)
+    else:
+      result = matchType(c, last(f), a, m)
+  of tyBuiltInTypeClass:
+    let target = f.genericHead.kind
+    result = a.skipTypes(ignorableForArgType).reduceToBase.kind == target
+  of tyOr:
+    if a.kind == tyOr:
+      var covered = 0
+      for ff in traverseTyOr(f):
+        for aa in traverseTyOr(a):
+          m.bindings = m.bindings.newTypeMapLayer()
+          let r = matchType(c, ff, aa, m)
+          if r:
+            inc covered
+            break
+          m.bindings.setToPreviousLayer()
+
+      result = covered >= a.kidsLen
+    else:
+      for ff in f.kids:
+        m.bindings = m.bindings.newTypeMapLayer()
+        result = matchType(c, ff, a, m)
+        if result: break # and remember the binding!
+        m.bindings.setToPreviousLayer()
   else:
     result = false
+  if result and ao.kind == tyGenericParam:
+    let bf = if f.isSelf: m.potentialImplementation else: f
+    if bindParam(c, m, ao, bf):
+      when logBindings: echo " ^ reverse binding"
+
+proc checkConstraint(c: PContext; f, a: PType; m: var MatchCon): bool =
+  result = matchType(c, f, a, m) or matchType(c, a, f, m)
 
 proc matchReturnType(c: PContext; f, a: PType; m: var MatchCon): bool =
   ## Like 'matchType' but with extra logic dealing with proc return types
@@ -290,30 +432,38 @@ proc matchReturnType(c: PContext; f, a: PType; m: var MatchCon): bool =
   elif a == nil:
     result = false
   else:
-    result = matchType(c, f, a, m)
+    result = checkConstraint(c, f, a, m)
 
 proc matchSym(c: PContext; candidate: PSym, n: PNode; m: var MatchCon): bool =
   ## Checks if 'candidate' matches 'n' from the concept body. 'n' is a nkProcDef
   ## or similar.
 
   # watch out: only add bindings after a completely successful match.
-  let oldLen = m.inferred.len
+  m.bindings = m.bindings.newTypeMapLayer()
 
   let can = candidate.typ.n
-  let con = n[0].sym.typ.n
-
+  let con = defSignatureType(n).n
   if can.len < con.len:
     # too few arguments, cannot be a match:
     return false
-
+  
+  if can.len > con.len:
+    # too many arguments (not optional)
+    for i in con.len ..< can.len:
+      if can[i].sym.ast == nil:
+        return false
+  
+  when defined(debugConcepts):
+    echo "considering: ", renderTree(candidate.procDefSignature), " ", candidate.magic
+  
   let common = min(can.len, con.len)
   for i in 1 ..< common:
-    if not matchType(c, con[i].typ, can[i].typ, m):
-      m.inferred.setLen oldLen
+    if not checkConstraint(c, con[i].typ, can[i].typ, m):
+      m.bindings.setToPreviousLayer()
       return false
-
-  if not matchReturnType(c, n[0].sym.typ.returnType, candidate.typ.returnType, m):
-    m.inferred.setLen oldLen
+  
+  if not matchReturnType(c, n.defSignatureType.returnType, candidate.typ.returnType, m):
+    m.bindings.setToPreviousLayer()
     return false
 
   # all other parameters have to be optional parameters:
@@ -321,7 +471,7 @@ proc matchSym(c: PContext; candidate: PSym, n: PNode; m: var MatchCon): bool =
     assert can[i].kind == nkSym
     if can[i].sym.ast == nil:
       # has too many arguments one of which is not optional:
-      m.inferred.setLen oldLen
+      m.bindings.setToPreviousLayer()
       return false
 
   return true
@@ -329,13 +479,14 @@ proc matchSym(c: PContext; candidate: PSym, n: PNode; m: var MatchCon): bool =
 proc matchSyms(c: PContext, n: PNode; kinds: set[TSymKind]; m: var MatchCon): bool =
   ## Walk the current scope, extract candidates which the same name as 'n[namePos]',
   ## 'n' is the nkProcDef or similar from the concept that we try to match.
+  result = false
   var candidates = searchScopes(c, n[namePos].sym.name, kinds)
   searchImportsAll(c, n[namePos].sym.name, kinds, candidates)
   for candidate in candidates:
-    #echo "considering ", typeToString(candidate.typ), " ", candidate.magic
     m.magic = candidate.magic
-    if matchSym(c, candidate, n, m): return true
-  result = false
+    if matchSym(c, candidate, n, m):
+      result = true
+      break
 
 proc conceptMatchNode(c: PContext; n: PNode; m: var MatchCon): bool =
   ## Traverse the concept's AST ('n') and see if every declaration inside 'n'
@@ -368,7 +519,48 @@ proc conceptMatchNode(c: PContext; n: PNode; m: var MatchCon): bool =
     # error was reported earlier.
     result = false
 
-proc conceptMatch*(c: PContext; concpt, arg: PType; bindings: var LayeredIdTable; invocation: PType): bool =
+proc fixBindings(bindings: var LayeredIdTable; concpt: PType; invocation: PType; m: var MatchCon) =
+  # invocation != nil means we have a non-atomic concept:
+  if invocation != nil and invocation.kind == tyGenericInvocation:
+    assert concpt.sym.typ.kind == tyGenericBody
+    
+    for i in 0 .. concpt.sym.typ.len - 1:
+      let thisSym = concpt.sym.typ[i]
+      if lookup(bindings, thisSym) != nil:
+        # dont trust the bindings over existing ones
+        continue
+      let found = m.bindings.lookup(thisSym)
+      if found != nil:
+        when logBindings: echo "Invocation bind: ", thisSym, " ", found
+        bindings.put(thisSym, found)
+    
+    # bind even more generic parameters
+    let genBody = invocation.base
+    assert genBody.kind == tyGenericBody
+    for i in FirstGenericParamAt ..< invocation.kidsLen:
+      let bpram = genBody[i - 1]
+      if lookup(bindings, invocation[i]) != nil:
+        # dont trust the bindings over existing ones
+        continue
+      let boundV = lookup(bindings, bpram)
+      when logBindings: echo "generic body bind: '", invocation[i], "' '", boundV, "'"
+      if boundV != nil:
+        bindings.put(invocation[i], boundV)
+  bindings.put(concpt, m.potentialImplementation)
+
+proc processConcept(c: PContext; concpt, invocation: PType, bindings: var LayeredIdTable; m: var MatchCon): bool =
+  m.bindings = m.bindings.newTypeMapLayer()
+  if invocation != nil and invocation.kind == tyGenericInst:
+    let genericBody = invocation.base
+    for i in 1..<invocation.kidsLen-1:
+      # instGenericContainer can bind `tyVoid`
+      if invocation[i].kind != tyVoid:
+        bindParam(c, m, genericBody[i-1], invocation[i])
+  result = conceptMatchNode(c, concpt.conceptBody, m)
+  if result and mfDontBind notin m.flags:
+    fixBindings(bindings, concpt, invocation, m)
+
+proc conceptMatch*(c: PContext; concpt, arg: PType; bindings: var LayeredIdTable; invocation: PType, flags: set[MatchFlags] = {}): bool =
   ## Entry point from sigmatch. 'concpt' is the concept we try to match (here still a PType but
   ## we extract its AST via 'concpt.n.lastSon'). 'arg' is the type that might fulfill the
   ## concept's requirements. If so, we return true and fill the 'bindings' with pairs of
@@ -377,28 +569,16 @@ proc conceptMatch*(c: PContext; concpt, arg: PType; bindings: var LayeredIdTable
   ## `C[S, T]` parent type that we look for. We need this because we need to store bindings
   ## for 'S' and 'T' inside 'bindings' on a successful match. It is very important that
   ## we do not add any bindings at all on an unsuccessful match!
-  if arg.containsUnresolvedType:
-    return false
-  var m = MatchCon(inferred: @[], potentialImplementation: arg, concpt: concpt)
-  result = conceptMatchNode(c, concpt.n.lastSon, m)
-  if result:
-    for (a, b) in m.inferred:
-      if b.kind == tyGenericParam:
-        var dest = b
-        while true:
-          dest = existingBinding(m, dest)
-          if dest == nil or dest.kind != tyGenericParam: break
-        if dest != nil:
-          bindings.put(a, dest)
-          when logBindings: echo "A bind ", a, " ", dest
-      else:
-        bindings.put(a, b)
-        when logBindings: echo "B bind ", a, " ", b
-    # we have a match, so bind 'arg' itself to 'concpt':
-    bindings.put(concpt, arg)
-    # invocation != nil means we have a non-atomic concept:
-    if invocation != nil and arg.kind == tyGenericInst and invocation.kidsLen == arg.kidsLen-1:
-      # bind even more generic parameters
-      assert invocation.kind == tyGenericInvocation
-      for i in FirstGenericParamAt ..< invocation.kidsLen:
-        bindings.put(invocation[i], arg[i])
+  var m = MatchCon(bindings: bindings, potentialImplementation: arg, concpt: concpt, flags: flags)
+  if arg.isConcept:
+    result = conceptsMatch(c, concpt.reduceToBase, arg.reduceToBase, m) >= mkSubset
+  elif arg.acceptsAllTypes:
+    # XXX: I think this is wrong, or at least partially wrong. Can still test ambiguous types
+    result = false
+  elif mfCheckGeneric in m.flags:
+    # prioritize concepts the least. Specifically if the arg is not a catch all as per above
+    result = true
+  else:
+    result = processConcept(c, concpt, invocation, bindings, m)
+
+  
diff --git a/compiler/layeredtable.nim b/compiler/layeredtable.nim
index 565fb95464..61a86cff84 100644
--- a/compiler/layeredtable.nim
+++ b/compiler/layeredtable.nim
@@ -1,4 +1,4 @@
-import std/tables
+import std/[tables]
 import ast
 
 type
@@ -53,6 +53,15 @@ proc setToPreviousLayer*(pt: var LayeredIdTable) {.inline.} =
       let tmp = pt.nextLayer[]
       pt = tmp
 
+iterator pairs*(pt: LayeredIdTable): (ItemId, PType) =
+  var tm = pt
+  while true:
+    for (k, v) in pairs(tm.topLayer):
+      yield (k, v)
+    if tm.nextLayer == nil:
+      break
+    tm.setToPreviousLayer
+
 proc lookup(typeMap: ref LayeredIdTableObj, key: ItemId): PType =
   result = nil
   var tm = typeMap
diff --git a/compiler/semcall.nim b/compiler/semcall.nim
index 92276b8487..0b1236b254 100644
--- a/compiler/semcall.nim
+++ b/compiler/semcall.nim
@@ -144,7 +144,6 @@ proc pickBestCandidate(c: PContext, headSymbol: PNode,
   while true:
     determineType(c, sym)
     z = initCandidate(c, sym, initialBinding, scope, diagnosticsFlag)
-
     # this is kinda backwards as without a check here the described
     # problems in recalc would not happen, but instead it 100%
     # does check forever in some cases
@@ -184,7 +183,7 @@ proc pickBestCandidate(c: PContext, headSymbol: PNode,
       # 1) new symbols are discovered but the loop ends before we recalc
       # 2) new symbols are discovered and resemmed forever
       # not 100% sure if these are possible though as they would rely
-      #  on somehow introducing a new overload during overload resolution
+      # on somehow introducing a new overload during overload resolution
 
       # Symbol table has been modified. Restart and pre-calculate all syms
       # before any further candidate init and compare. SLOW, but rare case.
diff --git a/compiler/semtypes.nim b/compiler/semtypes.nim
index ea150a4068..8bca77add5 100644
--- a/compiler/semtypes.nim
+++ b/compiler/semtypes.nim
@@ -1289,12 +1289,14 @@ proc liftParamType(c: PContext, procKind: TSymKind, genericParams: PNode,
         paramType[i] = lifted
         result = paramType
         result.last.shouldHaveMeta
-
-    let liftBody = recurse(paramType.skipModifier, true)
-    if liftBody != nil:
-      result = liftBody
-      result.flags.incl tfHasMeta
-      #result.shouldHaveMeta
+    if paramType.isConcept:
+      return addImplicitGeneric(c, paramType, paramTypId, info, genericParams, paramName)
+    else:
+      let liftBody = recurse(paramType.skipModifier, true)
+      if liftBody != nil:
+        result = liftBody
+        result.flags.incl tfHasMeta
+        #result.shouldHaveMeta
 
   of tyGenericInvocation:
     result = nil
@@ -1308,7 +1310,6 @@ proc liftParamType(c: PContext, procKind: TSymKind, genericParams: PNode,
       # this may happen for proc type appearing in a type section
       # before one of its param types
       return
-
     if body.last.kind == tyUserTypeClass:
       let expanded = instGenericContainer(c, info, paramType,
                                           allowMetaTypes = true)
diff --git a/compiler/semtypinst.nim b/compiler/semtypinst.nim
index 6c81f8ac7b..4637ea4046 100644
--- a/compiler/semtypinst.nim
+++ b/compiler/semtypinst.nim
@@ -608,10 +608,13 @@ proc replaceTypeVarsTAux(cl: var TReplTypeVars, t: PType, isInstValue = false):
   result = t
   if t == nil: return
 
+  var et = t
+  if t.isConcept:
+    et = t.reduceToBase
   const lookupMetas = {tyStatic, tyGenericParam, tyConcept} + tyTypeClasses - {tyAnything}
-  if t.kind in lookupMetas or
-      (t.kind == tyAnything and tfRetType notin t.flags):
-    let lookup = cl.typeMap.lookup(t)
+  if et.kind in lookupMetas or
+      (et.kind == tyAnything and tfRetType notin et.flags):
+    let lookup = cl.typeMap.lookup(et)
     if lookup != nil: return lookup
 
   case t.kind
diff --git a/compiler/sigmatch.nim b/compiler/sigmatch.nim
index ddf696bec0..47d155e192 100644
--- a/compiler/sigmatch.nim
+++ b/compiler/sigmatch.nim
@@ -20,6 +20,7 @@ import std/[intsets, strutils, tables]
 when defined(nimPreviewSlimSystem):
   import std/assertions
 
+
 type
   MismatchKind* = enum
     kUnknown, kAlreadyGiven, kUnknownNamedParam, kTypeMismatch, kVarNeeded,
@@ -94,6 +95,7 @@ type
     trNoCovariance
     trBindGenericParam  # bind tyGenericParam even with trDontBind
     trIsOutParam
+    trCheckGeneric
 
   TTypeRelFlags* = set[TTypeRelFlag]
 
@@ -297,9 +299,9 @@ proc checkGeneric(a, b: TCandidate): int =
   var winner = 0
   for aai, bbi in underspecifiedPairs(aa, bb, 1):
     var ma = newCandidate(c, bbi)
-    let tra = typeRel(ma, bbi, aai, {trDontBind})
+    let tra = typeRel(ma, bbi, aai, {trDontBind, trCheckGeneric})
     var mb = newCandidate(c, aai)
-    let trb = typeRel(mb, aai, bbi, {trDontBind})
+    let trb = typeRel(mb, aai, bbi, {trDontBind, trCheckGeneric})
     if tra == isGeneric and trb in {isNone, isInferred, isInferredConvertible}:
       if winner == -1: return 0
       winner = 1
@@ -363,6 +365,8 @@ proc sumGeneric(t: PType): int =
         result += sumGeneric(a)
       break
     else:
+      if t.isConcept:
+        result += t.reduceToBase.conceptBody.len
       break
 
 proc complexDisambiguation(a, b: PType): int =
@@ -1138,6 +1142,24 @@ proc isCovariantPtr(c: var TCandidate, f, a: PType): bool =
   else:
     return false
 
+proc enterConceptMatch(c: var TCandidate; f,a: PType, flags: TTypeRelFlags): TTypeRelation =
+  var
+    conceptFlags: set[MatchFlags] = {}
+    container: PType = nil
+    concpt = f
+  if concpt.kind != tyConcept:
+    container = concpt
+    concpt = container.reduceToBase
+  if trDontBind in flags:
+    conceptFlags.incl mfDontBind
+  if trCheckGeneric in flags:
+    conceptFlags.incl mfCheckGeneric
+  let mres = concepts.conceptMatch(c.c, concpt, a, c.bindings, container, flags = conceptFlags)
+  if mres:
+    isGeneric
+  else:
+    isNone
+
 when false:
   proc maxNumericType(prev, candidate: PType): PType =
     let c = candidate.skipTypes({tyRange})
@@ -1643,8 +1665,10 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
 
     let roota = if skipBoth or deptha > depthf: a.skipGenericAlias else: a
     let rootf = if skipBoth or depthf > deptha: f.skipGenericAlias else: f
-
-    if a.kind == tyGenericInst:
+    
+    if f.isConcept:
+      result = enterConceptMatch(c, rootf, roota, flags)
+    elif a.kind == tyGenericInst:
       if roota.base == rootf.base:
         let nextFlags = flags + {trNoCovariance}
         var hasCovariance = false
@@ -1715,7 +1739,7 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
     var x = a.skipGenericAlias
     if x.kind == tyGenericParam and x.len > 0:
       x = x.last
-    let concpt = f[0].skipTypes({tyGenericBody})
+    let concpt = f.reduceToBase
     var preventHack = concpt.kind == tyConcept
     if x.kind == tyOwned and f[0].kind != tyOwned:
       preventHack = true
@@ -1748,9 +1772,8 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
           # Workaround for regression #4589
           if f[i].kind != tyTypeDesc: return
       result = isGeneric
-    elif x.kind == tyGenericInst and concpt.kind == tyConcept:
-      result = if concepts.conceptMatch(c.c, concpt, x, c.bindings, f): isGeneric
-               else: isNone
+    elif concpt.kind == tyConcept:
+      result = enterConceptMatch(c, f, x, flags)
     else:
       let genericBody = f[0]
       var askip = skippedNone
@@ -1758,7 +1781,7 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
       let aobj = x.skipToObject(askip)
       let fobj = genericBody.last.skipToObject(fskip)
       result = typeRel(c, genericBody, x, flags)
-      if result != isNone:
+      if result != isNone and concpt.kind != tyConcept:
         # see tests/generics/tgeneric3.nim for an example that triggers this
         # piece of code:
         #
@@ -1886,11 +1909,7 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
         else:
           result = isNone
   of tyConcept:
-    if a.kind == tyConcept and sameType(f, a):
-      result = isGeneric
-    else:
-      result = if concepts.conceptMatch(c.c, f, a, c.bindings, nil): isGeneric
-               else: isNone
+    result = enterConceptMatch(c, f, a, flags)
   of tyCompositeTypeClass:
     considerPreviousT:
       let roota = a.skipGenericAlias
@@ -2411,7 +2430,6 @@ proc paramTypesMatchAux(m: var TCandidate, f, a: PType,
 
   let oldInheritancePenalty = m.inheritancePenalty
   var r = typeRel(m, f, a)
-
   # This special typing rule for macros and templates is not documented
   # anywhere and breaks symmetry. It's hard to get rid of though, my
   # custom seqs example fails to compile without this:
diff --git a/compiler/types.nim b/compiler/types.nim
index 16853e5ffa..2acb164d4d 100644
--- a/compiler/types.nim
+++ b/compiler/types.nim
@@ -1515,6 +1515,20 @@ proc getSize*(conf: ConfigRef; typ: PType): BiggestInt =
   computeSizeAlign(conf, typ)
   result = typ.size
 
+proc isConcept*(t: PType): bool=
+  case t.kind
+  of tyConcept: true
+  of tyCompositeTypeClass:
+    t.hasElementType and isConcept(t.elementType)
+  of tyGenericBody:
+    t.typeBodyImpl.kind == tyConcept
+  of tyGenericInvocation, tyGenericInst:
+    if t.baseClass.kind == tyGenericBody:
+      t.baseClass.typeBodyImpl.kind == tyConcept
+    else:
+      t.baseClass.kind == tyConcept
+  else: false
+
 proc containsGenericTypeIter(t: PType, closure: RootRef): bool =
   case t.kind
   of tyStatic:
@@ -1525,6 +1539,8 @@ proc containsGenericTypeIter(t: PType, closure: RootRef): bool =
     return false
   of GenericTypes + tyTypeClasses + {tyFromExpr}:
     return true
+  of tyGenericInst:
+    return t.isConcept
   else:
     return false
 
@@ -2053,6 +2069,7 @@ proc genericRoot*(t: PType): PType =
 
 proc reduceToBase*(f: PType): PType =
   #[
+    Not recursion safe
     Returns the lowest order (most general) type that that is compatible with the input.
     E.g.
     A[T] = ptr object ... A -> ptr object
@@ -2077,7 +2094,7 @@ proc reduceToBase*(f: PType): PType =
     result = reduceToBase(f.typeBodyImpl)
   of tyUserTypeClass:
     if f.isResolvedUserTypeClass:
-      result = f.base  # ?? idk if this is right
+      result = f.base
     else:
       result = f.skipModifier
   of tyStatic, tyOwned, tyVar, tyLent, tySink:
diff --git a/doc/manual.md b/doc/manual.md
index 40b7b9f180..8eab6683d5 100644
--- a/doc/manual.md
+++ b/doc/manual.md
@@ -2927,6 +2927,97 @@ a parameter has different names between them.
 Not supplying the parameter name in such cases results in an
 ambiguity error.
 
+Concepts
+=========
+
+Concepts are a mechanism for users to define custom type classes that match other
+types based on a given set of bindings.
+
+```nim
+type
+  Comparable = concept # Atomic concept
+    proc cmp(a, b: Self): int
+  Indexable[I, T] = concept # Container concept
+    proc `[]`(x: Self; at: I): T
+    proc `[]=`(x: var Self; at: I; newVal: T)
+    proc len(x: Self): I
+  Index = concept
+    proc inc(x: var Self)
+    proc `<`(a, b: Self): bool
+proc sort*[I: Index; T: Comparable](x: var Indexable[I, T])
+```
+
+In the above example, `Comparable` and `Indexable` are types that will match any type that
+can can bind each definition declared in the concept body. The special `Self` type defined
+in the concept body refers to the type being matched, also called the "implementation" of 
+the concept. Implementations that match the concept are generic matches, and the concept 
+typeclasses themselves work in a similar way to generic type variables in that they are never
+concrete types themselves (even if they have concrete type parameters such as `Indexable[int, int]`)
+and expressions like `typeof(x)` in the body of `proc sort` from the above example will return the 
+type of the implementation, not the concept typeclass. Concepts are useful for providing information
+to the compiler in generic contexts, most notably for generic type checking, and as a tool for 
+[Overload resolution]. Generic type checking is forthcoming, so this will only explain overload
+resolution for now.
+
+In the example above, "atomic" and "container" concepts are mentioned. These kinds of concept
+are determined by the generic type variables of the concept. Atomic concepts` definitions contain
+only concrete types, and the `Self` type is inferred to be concrete. Container types are the same,
+under the condition that their generic variables are bound to concrete types and substituted appropriately.
+The programmer is free to define a concept that breaks these concreteness rules, thus making a "gray" concept:
+
+```nim
+type
+  Processor = concept
+    proc process[T](s: Self; data: T)
+```
+
+The above concept does not have generic variables, and its definition contains `T` which is not concrete.
+This kind of concept may disrupt the compiler's ability to type check generic contexts, but it is useful for
+overload resolution. The difference between `Indexable[I, T]` and `Processor` is that a given implementation
+is effectively described as an instantiation of `Indexable` (as in `Indexable[int, int]`) whereas a `Processor`
+concept describes an implementation designed to handle multiple different types of data `T`.
+
+Concept overload resolution
+-----------------------------
+
+When an operand's type is being matched to a concept, the operand's type  is set as the "potential
+implementation". For each definition in the concept body, overload resolution is performed by substituting `Self`
+for the potential implementation to try and find a match for each definition. If this succeeds, the concept 
+matches. Implementations do not need to exactly match the definitions in the concept. For example:
+
+```nim
+type
+  C1 = concept
+    proc p(s: Self; x: int)
+  Implementation = object
+
+proc p(x: Implementation; y: SomeInteger)
+proc spring(x: C1)
+spring(Implementation())
+```
+This will bind because `p(Implementation(), 0)` will bind. Conversely, container types will bind to
+less specific definitions if the generic constraints and bindings allow it, as per usual generic matching.
+
+Things start to get more complicated when overload resolution starts "Hierarchical Order Comparison"
+I.E. specificity comparison as per [Overload resolution]. In this state the compiler may be comparing
+all kinds of types and typeclasses with concepts as defined in the `proc` definitions of each overload.
+This leads to confusing and impractical behavior in most situations, so the rules are simplified. They are:
+
+1. if a concept is being compared with `T` or any type that accepts all other types (`auto`) the concept
+is more specific
+2. if the concept is being compared with another concept the result is deferred to [Concept subset matching]
+3. in any other case the concept is less specific then it's competitor 
+
+
+Concept subset matching
+-------------------------
+
+This type of matching is simple. When comparing concepts `C1` and `C2`, if all valid implementations of `C1`
+are also valid implementations of `C2` but not vice versa then `C1` is a subset of `C2`. This means that
+`C1` will match to `C2` and therefore the disambiguation process will prefer `C2` as it is more specific.
+If neither of them are subsets of one another, then the disambiguation proceeds to complexity analysis
+and the concept with the most definitions wins, if any. No definite winner is an ambiguity error at
+compile time.
 
 Statements and expressions
 ==========================
diff --git a/tests/concepts/conceptv2negative/tmarrget.nim b/tests/concepts/conceptv2negative/tmarrget.nim
new file mode 100644
index 0000000000..64d6b8c91a
--- /dev/null
+++ b/tests/concepts/conceptv2negative/tmarrget.nim
@@ -0,0 +1,12 @@
+discard """
+action: "reject"
+"""
+
+# stop mArrGet magic from giving everything `[]`
+type
+  C[T] = concept
+    proc `[]`(b: Self, i: int): T
+  A = object
+  
+proc p(a: C): int = assert false
+discard p(A())
diff --git a/tests/concepts/conceptv2negative/tmissingbind.nim b/tests/concepts/conceptv2negative/tmissingbind.nim
new file mode 100644
index 0000000000..78376aeaeb
--- /dev/null
+++ b/tests/concepts/conceptv2negative/tmissingbind.nim
@@ -0,0 +1,26 @@
+discard """
+action: "reject"
+"""
+
+#[
+  ArrayImpl is not Sizeable
+]#
+
+type
+  Sizeable = concept
+    proc size(s: Self): int
+  Buffer = concept
+    proc w(s: Self, data: Sizeable)
+  Serializable = concept
+    proc something(s: Self)
+    proc w(b: Buffer, s: Self)
+  BufferImpl = object
+  ArrayImpl = object
+
+proc something(s: ArrayImpl)= discard
+#proc size(s: ArrayImpl): int= discard
+proc w(x: BufferImpl, d: Sizeable)= discard
+
+proc spring(s: Buffer, data: Serializable)= discard
+
+spring(BufferImpl(), ArrayImpl())
diff --git a/tests/concepts/tconceptsv2.nim b/tests/concepts/tconceptsv2.nim
index 0db79c0269..5befd2fafa 100644
--- a/tests/concepts/tconceptsv2.nim
+++ b/tests/concepts/tconceptsv2.nim
@@ -5,7 +5,15 @@ B[system.int]
 A[system.string]
 A[array[0..0, int]]
 A[seq[int]]
-char
+100
+a
+b
+c
+a
+b
+c
+1
+2
 '''
 """
 import conceptsv2_helper
@@ -104,7 +112,7 @@ block: # simple recursion
     WritableImpl = object
 
   proc launch(a: var Buffer, b: Writable)= discard
-  proc put(x: var BufferImpl, i: object)= discard
+  proc put[T](x: var BufferImpl, i: T)= discard
   proc second(x: BufferImpl)= discard
   proc put(x: var Buffer, y: WritableImpl)= discard
 
@@ -122,7 +130,7 @@ block: # more complex recursion
     WritableImpl = object
 
   proc launch(a: var Buffer, b: Writable)= discard
-  proc put(x: var Buffer, i: object)= discard
+  proc put[T](x: var Buffer, i: T)= discard
   proc put(x: var BufferImpl, i: object)= discard
   proc second(x: BufferImpl)= discard
   proc put(x: var Buffer, y: WritableImpl)= discard
@@ -130,37 +138,320 @@ block: # more complex recursion
   var a = BufferImpl[5]()
   launch(a, WritableImpl())
 
-block:  # capture p1[T]
+block: # co-dependent concepts
   type
-    A[T] = object
-    C = concept
-      proc p1(x: Self, i: int): float
+    Writable = concept
+      proc w(b: var Buffer; s: Self): int
+    Buffer = concept
+      proc w(s: var Self; data: Writable): int
+    SizedWritable = concept
+      proc size(x: Self): int
+      proc w(b: var Buffer, x: Self): int
+    BufferImpl = object
+    
+  proc w(x: var BufferImpl, d: int): int = return 100
+  proc size(d: int): int = sizeof(int)
 
-  proc p1[T](a: A[T], idx: int): T = default(T)
-  proc p(a: C): int = discard
-  proc p[T](a: T):int = assert false
+  proc p(b: var Buffer, data: SizedWritable): int =
+    b.w(data)
 
-  discard p(A[float]())
+  var b = BufferImpl()
+  echo p(b, 5)
 
-block:  # mArrGet binding
+block: # indirect concept matching
+  type
+    Sizeable = concept
+      proc size(s: Self): int
+    Buffer = concept
+      proc w(s: Self, data: Sizeable)
+    Serializable = concept
+      proc something(s: Self)
+      proc w(b: Buffer, s: Self)
+    BufferImpl = object
+    ArrayImpl = object
+
+  proc something(s: ArrayImpl)= discard
+  proc size(s: ArrayImpl): int= discard
+
+  proc w(x: BufferImpl, d: Sizeable)= discard
+
+  proc spring(s: Buffer, data: Serializable)=discard
+
+  spring(BufferImpl(), ArrayImpl())
+
+block: # instantiate even when generic params are the same
   type
     ArrayLike[T] = concept
       proc len(x: Self): int
       proc `[]`(b: Self, i: int): T
+  proc p[T](x: ArrayLike[T])=
+    for k in x:
+      echo k
+  # For this test to work the second call's instantiation has to be incompatible with the first on the back end
+  p(['a','b','c'])
+  p("abc")
 
-  proc p[T](a: ArrayLike[T]): int= discard
-  discard p([1,2])
+block: # reject improper generic variables in candidates
+  type
+    ArrayLike[T] = concept
+      proc len(x: Self): int
+      proc g(b: Self, i: int): T
+    FreakString = concept
+      proc len(x: Self): int
+      proc characterSize(s: Self): int 
+    A = object
+
+  proc g[T, H](s: T, i: H): H = default(T)
+  proc len(s: A): int = discard
+  proc characterSize(s: A): int = discard
+  
+  proc p(symbol: ArrayLike[char]): int = assert false
+  proc p(symbol: FreakString): int=discard
+  
+  discard p(A())
+
+block: # typerel disambiguation by concept subset
+  type
+    ArrayLike[T] = concept
+      proc len(x: Self): int
+      proc characterSize(s: Self): int
+    FreakString = concept
+      proc len(x: Self): int
+      proc characterSize(s: Self): int
+      proc tieBreaker(s: Self, j: int): float
+    A = object
+
+  proc len(s: A): int = discard
+  proc characterSize(s: A): int = discard
+  proc tieBreaker(s: A, h: int):float = 0.0
+  
+  proc p(symbol: ArrayLike[char]): int = assert false
+  proc p(symbol: FreakString): int=discard
+  
+  discard p(A())
+
+block:  # tie break via sumGeneric
+  type
+    C1 = concept
+      proc p1(x: Self, b: int)
+      proc p2(x: Self, b: float)
+      proc p3(x: Self, b: string)
+    C2 = concept
+      proc b1(x: Self, b: int)
+      proc b2(x: Self, b: float)
+    A = object
+  
+  proc p1(x: A, b: int)=discard
+  proc p2(x: A, b: float)=discard
+  proc p3(x: A, b: string)=discard
+  
+  proc b1(x: A, b: int)=discard
+  proc b2(x: A, b: float)=discard
+  
+  proc p(symbol: C1): int = discard
+  proc p(symbol: C2): int = assert false
+  
+  discard p(A())
+
+block: # not type
+  type
+    C1 = concept
+      proc p(s: Self, a: int)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: not float)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # not type parameterized
+  type
+    C1[T: not int] = concept
+      proc p(s: Self, a: T)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: float)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # typedesc
+  type
+    C1 = concept
+      proc p(s: Self, a: typedesc[SomeInteger])
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: typedesc)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+
+block: # or
+  type
+    C1 = concept
+      proc p(s: Self, a: int | float)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: int | float | string)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # or mixed generic param
+  type
+    C1 = concept
+      proc p(s: Self, a: int | float)
+    C1Impl = object
+    
+  proc p[T: string | float](x: C1Impl, a: int | T) = discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # or parameterized
+  type
+    C1[T: int | float | string] = concept
+      proc p(s: Self, a: T)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: int | float)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # unconstrained param
+  type
+    A = object
+    C1[T] = concept
+      proc p(s: Self, a: T)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: A)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # unconstrained param sanity check
+  type
+    A = object
+    C1[T: auto] = concept
+      proc p(s: Self, a: T)
+    C1Impl = object
+    
+  proc p(x: C1Impl, a: A)= discard
+  proc spring(x: C1)= discard
+
+  spring(C1Impl())
+
+block: # exact nested concept binding
+  type
+    Sizeable = concept
+      proc size(s: Self): int
+    Buffer = concept
+      proc w(s: Self, data: Sizeable)
+    Serializable = concept
+      proc w(b: Buffer, s: Self)
+    ArrayLike = concept
+      proc len(s: Self): int
+    ArrayImpl = object
+
+  proc len(s: ArrayImpl): int = discard
+  proc w(x: Buffer, d: ArrayLike)=discard
+
+  proc spring(data: Serializable)=discard
+  spring(ArrayImpl())
 
 block:
   type
-    A[T] = object
-    ArrayLike[T] = concept
-      proc len(x: Self): int
-      proc `[]`(b: Self, i: int): T
-      proc tell(s: Self, x: A[int])
-  
-  proc tell(x: string, h: A[int])= discard
+    StaticallySized = concept
+      proc staticSize(x: typedesc[Self]): int
+      proc dynamicSize(x: Self): int
+    DynamicallySized = concept
+      proc dynamicSize(x: Self): int
 
-  proc spring[T](w: ArrayLike[T])= echo T
-  
-  spring("hi")
+  proc dynamicSize(a: SomeInteger): int = 5
+  proc read[T: DynamicallySized](a: var T): int = 1
+  proc read[T: SomeInteger](a: var T): int = 2
+
+  var a: uint16
+  assert read(a) == 2
+
+block:
+  type
+    A[X, Y] = object
+      x: X
+      y: Y
+    C1 = concept
+      proc p(z: var Self)
+    C2 = concept
+      proc g(x: var Self, y: int)
+    C3 = C1 and C2
+    C4 = concept
+      proc h(x: Self): C3
+
+  proc p[X, Y](z: var A[int, float]) = discard
+  proc g[X, Y](z: var A[X, Y], y: int) = discard
+  proc h[X, Y](z: var A[X, Y]): A[X, Y] = discard
+
+  proc spring(x: C4) = discard
+  var d = A[int, float]()
+  d.spring()
+
+block:
+  type
+    A[X, Y] = object
+      x: X
+      y: Y
+    B = object
+    C1 = concept
+      proc p(z: var Self, d: A[int, float])
+
+  proc p[X: int; Y: float](x: var B, y: A[X, Y]) = discard
+  proc spring(x: var C1) = discard
+  var d = B()
+  d.spring()
+
+block:
+  type
+    A = object
+    C1 = concept
+      proc p(s: Self; x: auto)
+    C2[T: int] = concept
+      proc p(s: Self; x: T)
+    Impl = object
+
+  proc p(n: Impl; i: int) = discard
+
+  proc spring(x: C1): int = 1
+  proc spring(x: C2): int = 2
+
+  assert spring(Impl()) == 2
+
+# this code fails inside a block for some reason
+type Indexable[T] = concept
+  proc `[]`(t: Self, i: int): T
+  proc len(t: Self): int
+
+iterator items[T](t: Indexable[T]): T =
+  for i in 0 ..< t.len:
+    yield t[i]
+
+type Enumerable[T] = concept
+  iterator items(t: Self): T
+
+proc echoAll[T](t: Enumerable[T]) =
+  for item in t:
+    echo item
+
+type DummyIndexable[T] = distinct seq[T]
+
+proc `[]`[T](t: DummyIndexable[T], i: int): T =
+  seq[T](t)[i]
+
+proc len[T](t: DummyIndexable[T]): int =
+  seq[T](t).len
+
+
+let dummyIndexable = DummyIndexable(@[1, 2])
+echoAll(dummyIndexable)